Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
12
 Projects Packages Public Activity Starred Repositories
9
aniva pushed to doc/readme at aniva/Pantograph 2024-04-15 19:57:21 -07:00
52e5b5df50 doc: README.md fix
aniva created branch doc/readme in aniva/Pantograph 2024-04-15 19:57:21 -07:00
aniva commented on pull request aniva/Pantograph#72 2024-04-15 13:03:31 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

Waiting for this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaborator.20and.20.40/near/433364676

aniva deleted branch lib/mkOptions from aniva/Pantograph 2024-04-15 12:58:10 -07:00
aniva pushed to dev at aniva/Pantograph 2024-04-15 12:58:09 -07:00
adbb07af2d fix: Option setting in REPL
aniva merged pull request aniva/Pantograph#71 2024-04-15 12:58:08 -07:00
fix: Option setting in REPL
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-15 12:56:40 -07:00
7aa7e6d7e9 feat: Library interface for mapply
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-15 12:47:18 -07:00
dbd54f7679 feat: Implement the mapply tactic
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-14 15:41:14 -07:00
75b4648ba9 feat: mapply stub
aniva created pull request aniva/Pantograph#72 2024-04-13 19:43:04 -07:00
feat: Motivated apply (mapply) tactic
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-13 19:42:12 -07:00
b954f12526 refactor: Move all tactic operations to the bottom
aniva created branch goal/mapply in aniva/Pantograph 2024-04-13 19:42:12 -07:00
aniva created pull request aniva/Pantograph#71 2024-04-12 22:41:12 -07:00
fix: Option setting in REPL
aniva pushed to lib/mkOptions at aniva/Pantograph 2024-04-12 22:40:02 -07:00
adbb07af2d fix: Option setting in REPL
aniva created branch lib/mkOptions in aniva/Pantograph 2024-04-12 22:40:02 -07:00
aniva deleted branch goal/let from aniva/Pantograph 2024-04-12 21:42:34 -07:00
aniva pushed to dev at aniva/Pantograph 2024-04-12 21:42:34 -07:00
72dd20ea87 Merge pull request 'feat: Let tactic' (#70) from goal/let into dev
614b9aa4ae Merge branch 'dev' into goal/let
b45b90b810 test: Metavariable name matches in let
77907fd060 feat: `goalLet` function
4ee955c21f test: Tests the `let` tactic
Compare 5 commits »
aniva merged pull request aniva/Pantograph#70 2024-04-12 21:42:33 -07:00
feat: Let tactic
aniva pushed to goal/let at aniva/Pantograph 2024-04-12 21:42:05 -07:00
614b9aa4ae Merge branch 'dev' into goal/let
07094730b7 Merge pull request 'feat: Option to collect dependent metavariables' (#69) from serial/goal into dev
4b01af7cef Merge branch 'dev' into serial/goal
e5d55e31ff feat: Print expression dependent mvars
8e377c2092 refactor: CamelCase rename
Compare 6 commits »
aniva pushed to goal/let at aniva/Pantograph 2024-04-12 21:41:35 -07:00
b45b90b810 test: Metavariable name matches in let