- Stanford University Centaur Group
- https://leni.sh
-
Admin of this website
- Joined on
2023-08-21
472cd54868
Merge pull request 'refactor: Cleanup the congruence tactics' (#81) from tactic/congruence into dev
fbe6e8fcb3
Merge branch 'dev' into tactic/congruence
aceee85b05
Merge branch 'env/inspect' into tactic/congruence
f80d90ce87
fix: Goal diag missing newline character
b3a60fcea8
refactor: Rename TacticExecute to SyntheticTactic
refactor: Cleanup the congruence tactics
fbe6e8fcb3
Merge branch 'dev' into tactic/congruence
361e2e8926
Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
feat: Handling of universe level names in elab
361e2e8926
Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
8707dbc9bb
fix: aux lemmas in env inspect
fix: aux lemmas in env inspect
aceee85b05
Merge branch 'env/inspect' into tactic/congruence
8707dbc9bb
fix: aux lemmas in env inspect
fix: aux lemmas in env inspect
refactor: Cleanup the congruence tactics
bd20bf76da
Merge pull request 'feat: Elementarized tactics with motives, congruence, and absurdity' (#72) from goal/mapply into dev
2d2cf75183
Merge branch 'dev' into goal/mapply
c0e6e3ec39
Merge branch 'parse/level' into goal/mapply
773a0afbd8
feat: Handling of universe level names in elab
3a53493089
feat: Show delayed assignment in goal diag
feat: Elementarized tactics with motives, congruence, and absurdity