Simple Node.js wrapper for Lean 4 theorem prover
npm install leannode-coreA minimal Node.js wrapper for the Lean 4 theorem prover.
``bash`
npm install leannode-core
Prerequisites: You must have Lean 4 installed and available in your PATH.
`javascript
const LeanRunner = require('leannode-core');
// Basic evaluation
const result = await LeanRunner.run('#eval 2 + 3');
console.log(result.stdout); // "5"
// Define and evaluate
const code =
def factorial : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * factorial n
#eval factorial 5;
const result = await LeanRunner.run(code);
console.log(result.stdout); // "120"
`
Executes Lean code and returns a promise with the result.
Parameters:
- leanCode (string): The Lean code to executeoptions
- (object, optional):args
- (array): Additional command line arguments for Leancwd
- (string): Working directory for the Lean processenv
- (object): Environment variables
Returns:
Promise resolving to:
`javascript`
{
stdout: string, // Standard output from Lean
stderr: string, // Standard error from Lean
exitCode: number // Process exit code (0 = success)
}
`bash``
npm test
MIT