lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
Originally from `module.cpp` (RIP) ---- - Persistent `set_option`. We want to be able to store the option settings in .olean files. The main issue is conflict between imported modules. That...
@Kha when `panic` is evaluated by the interpreter, the execution is interrupted as expected. However, all trace messages produced using `dbgTrace` are lost because the `#eval` command implementation redirects stdout...
Consider the following variants of a `cache` function ```lean import Lean set_option trace.compiler.ir.result true open Lean structure State where keys : Array Expr results : Array Expr abbrev M :=...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
We store the Lean wrappers of stdin/stdout/stderr in thread-local variables to support redirection as in `withStdin/...`. New threads spawned within these functions should inherit these variables. Note that if a...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
The current standard library in the Lean core is lacking many common utility functions. One way to go about fleshing it out is to allow the community to contributed useful...
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
As some of the Lean 3 widget features are [rolling in](https://github.com/leanprover/vscode-lean4/pull/37), we should decide on the next step. I think a good one would be to provide a typeclass which...
We had this option in Lean 3.
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover