lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
The docstring is for the user of the function, who doesn't need to care that it is a reference implementation. Instead, make the "reference implementation" bit a comment in the...
Depends on #3590 Closes #3458
This PR partly addresses #3458, by adding an option `autoPromoteIndices` to turn off the promotion of fixed indices to parameters. The actual fix for the issue is in a separate...
This coercion caused difficult-to-diagnose bugs sometimes. Because there are some situations where converting a string to a name should be done by parsing the string, and others where it should...
Implementation of the lean side of #3567. Passing `--continue-on-error` to lean will cause it to produce an `.olean` file even if the file had an error, but it will still...
This is still a work in progress.
It's often confusing how `fun x y => ?foo` elaborates as `fun x y => ?m.123 x y`, with no way to see how `?m.123` is connected to `?foo`. This...
This characterizes `toInt` in terms of `toNat`. This PR is stacked on https://github.com/leanprover/lean4/pull/3480 to write the theorems in a style that includes the width zero case.
(In progress; fully experimental.)
Change the invariant `Q` to only have to be defined for `Fin (w+1)`, rather than all `Nat`s. This is a strict generalization, and makes defining an invariant that doesn't necessarily...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover