lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
This supersedes https://github.com/leanprover/std4/pull/664, and adds lemmas that mirror `ofNat_{add,sub}_ofNat` for ult, ule.
Closes #3386 Currently, when generating the signature of an injectivity lemma for a certain constructor `c : forall xs, Foo a_1 ... a_n`, `mkInjectiveTheoremTypeCore?` will differentiate between variables which are...
This is still experimental, but it implements identifier support in auto tactics "in the obvious way". It also converts `quoteAutoTactic` to generate Expr directly instead of going via syntax (this...
Work-in-progress PR for an alternative TOML configuration file for basic packages. ### Task list * [x] TOML parser * [x] TOML data types * [x] TOML elaborator (Syntax -> data...
It is the second linter framework from Std. It runs *after* declarations have been made, and e.g. can verify global properties of simp sets. WIP, there are a number of...
This small PR changes the error message that triggers when simp reaches the `maxSteps` parameter to mention that this is a configurable setting and say what the name of the...
This PR adds support for requests from the server to the client in the language server. It is based on #3014 and was developed during an experiment for #3247 that...
We are planning to introduce a new package to core for functionality that a) is not strictly necessary for building Lean (so it should not be in `Init` or `Lean`)...
Sends a diagnostic informing the user to run Restart File when a file dependency is saved. Based on #3014 because this feature was easier to implement with the new architecture....
`FileMap.lines` is an array that seems to be manually managed to have the form `#[1, 2, ..., n-1, n-1]` with same length as `FileMap.positions`. Remove this structure field in favour...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover