- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
doc: Change license to Apache2
doc: Change license to Apache2
chore: Update Lean4 upstream to unofficial flake
Incremental and intercepted parsing of Lean code
a11127a64e
Merge pull request 'feat: Capture environment in drafting' (#113) from frontend/environment into dev
72e41e1e1e
Merge branch 'dev' into frontend/environment
946e688dec
test(frontend): Environment capture
5a2ae880f4
feat: Capture environment in drafting
feat: Capture environment in drafting
feat: Enable environment capture during
frontend.process
72e41e1e1e
Merge branch 'dev' into frontend/environment
5b278d68d4
Merge pull request 'feat: Let tactic in REPL' (#111) from repl/tactic-let into dev
645d9c9250
feat: Let tactic in REPL
feat: Capture environment in drafting
In the future we could change sorrysToGoalState
to take a Environment
argument, but this looks fine.
5b278d68d4
Merge pull request 'feat: Let tactic in REPL' (#111) from repl/tactic-let into dev
645d9c9250
feat: Let tactic in REPL