- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
fix: Shield tactics from the environment generated by `frontend.process`
fix(repl): Elaborate with `errToSorry` as false by default
fix(goal): Prevent duplication in idempotent tactics
fix: Shield tactics from the environment generated by
frontend.process
Add documentation about what we cannot implement
Add unsafe detection in goal.print
We should also output messages after a tactic to service things such as trace_state
.
After each tactic, we can report whether the proof expression created in the mvars and delayed mvars have…