- Stanford University Centaur Group
- https://leni.sh
-
Admin of this website
- Joined on
2023-08-21
Enable direct expression evaluation in context
Exposed interface for MetaM context and state in #85.
Extraction of atomization step
Atomization is too tightly coupled to the user architecture. We'll not include it here in the forseeable future. Vide aniva/Trillium#124: A new Catenary library was…
Expose the
String.toName interface
Expose the
String.toName interface
The user should call into Lean's kernel directly for this kind of features. We'll not re-expose functions in the Lean kernel.
test: Use `lake test`. Retired `Makefile`
test: Use
lake test. Retired Makefile
feat: Prograde tactics
Fixed one of the old glaring bugs of the let tactic where the binder was not introduced. Fixed flake build failure.
Waiting for downstream testing in Trillium before merging.