- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
53f3c5d63d
fix: Use prompt_hostname instead of hostname
301b57ec06
Initial commit
feat: Elementarized tactics with motives, congruence, and absurdity
This breaks current metavariable resolution schema because the motive variable is delay assigned. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Force.20instantiate.20delay.…
fix: Linux sway and eww settings
feat: Emacs shell compatibility and SCAD mode