lean4lean
lean4lean copied to clipboard
digama0
Lean 4 kernel / 'external checker' written in Lean 4
Hi, I've been adding some documentation while trying to understand this implementation better. Regarding the FIXMEs, I've left them in for now just because I was curious if you have...
I got around to adding some more docs for the functions handling the checking/generation of inductive types. I also took the liberty to rename some variables in a few places...
This PR adds an optimization to the typechecker implementation to make better use of the `EquivManager` definitional equality cache by reusing free variables where possible. As a motivating example, suppose...
This PR dependabot (to check github actions updates) and update operation (to update lean toolchain) per 10 days added Some notes: - Uses: https://github.com/oliver-butterley/lean-update - each update either succeeds and...
