Leni Aniva aniva
  • Stanford University Centaur Group
  • https://leni.sh
  • Admin of this website

  • Joined on 2023-08-21
aniva deleted branch tactic/congruence from aniva/Pantograph 2024-06-23 13:35:38 -07:00
aniva pushed to dev at aniva/Pantograph 2024-06-23 13:35:38 -07:00
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
Compare 5 commits »
aniva merged pull request aniva/Pantograph#81 2024-06-23 13:35:36 -07:00
refactor: Cleanup the congruence tactics
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-23 13:35:17 -07:00
fbe6e8fcb3 Merge branch 'dev' into tactic/congruence
361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
Compare 2 commits »
aniva closed issue aniva/Pantograph#77 2024-06-23 13:34:03 -07:00
Unclear error message
aniva closed pull request aniva/Pantograph#79 2024-06-23 13:33:55 -07:00
feat: Handling of universe level names in elab
aniva deleted branch env/inspect from aniva/Pantograph 2024-06-23 13:33:38 -07:00
aniva pushed to dev at aniva/Pantograph 2024-06-23 13:33:37 -07:00
361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
8707dbc9bb fix: aux lemmas in env inspect
Compare 2 commits »
aniva merged pull request aniva/Pantograph#82 2024-06-23 13:33:35 -07:00
fix: aux lemmas in env inspect
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-16 13:46:23 -07:00
aceee85b05 Merge branch 'env/inspect' into tactic/congruence
8707dbc9bb fix: aux lemmas in env inspect
Compare 2 commits »
aniva created pull request aniva/Pantograph#82 2024-06-16 13:46:02 -07:00
fix: aux lemmas in env inspect
aniva created branch env/inspect in aniva/Pantograph 2024-06-16 13:45:36 -07:00
aniva pushed to env/inspect at aniva/Pantograph 2024-06-16 13:45:36 -07:00
8707dbc9bb fix: aux lemmas in env inspect
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-14 11:59:28 -07:00
f80d90ce87 fix: Goal diag missing newline character
aniva created pull request aniva/Pantograph#81 2024-06-13 14:25:45 -07:00
refactor: Cleanup the congruence tactics
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-13 14:25:12 -07:00
b3a60fcea8 refactor: Rename TacticExecute to SyntheticTactic
aniva created branch tactic/congruence in aniva/Pantograph 2024-06-13 14:25:12 -07:00
aniva deleted branch goal/mapply from aniva/Pantograph 2024-06-12 13:52:47 -07:00
aniva pushed to dev at aniva/Pantograph 2024-06-12 13:52:47 -07:00
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
Compare 42 commits »
aniva merged pull request aniva/Pantograph#72 2024-06-12 13:52:46 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity