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 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
aniva pushed to goal/mapply at aniva/Pantograph 2024-06-12 13:44:57 -07:00
2d2cf75183 Merge branch 'dev' into goal/mapply
67e7f22b0a Merge pull request 'feat: Extraction of tactics from compiler' (#76) from compile/tactic into dev
a2c5c7448c chore: Code simplification, version bump
855e771609 feat: Add compilation unit boundary command
b9b16ba0e9 refactor: Code cleanup
Compare 6 commits »
aniva pushed to goal/mapply at aniva/Pantograph 2024-06-11 15:21:46 -07:00
c0e6e3ec39 Merge branch 'parse/level' into goal/mapply
773a0afbd8 feat: Handling of universe level names in elab
Compare 2 commits »
aniva opened issue aniva/Pantograph#80 2024-06-11 15:07:12 -07:00
Expose the String.toName interface
aniva commented on issue aniva/Pantograph#77 2024-06-11 12:45:35 -07:00
Unclear error message

#79

aniva created pull request aniva/Pantograph#79 2024-06-11 12:45:29 -07:00
feat: Handling of universe level names in elab
aniva created branch parse/level in aniva/Pantograph 2024-06-11 12:45:07 -07:00
aniva pushed to parse/level at aniva/Pantograph 2024-06-11 12:45:07 -07:00
773a0afbd8 feat: Handling of universe level names in elab
aniva opened issue aniva/Pantograph#78 2024-06-10 13:03:06 -07:00
Add option for Meta.ppGoal
aniva commented on issue aniva/Pantograph#77 2024-06-10 13:01:20 -07:00
Unclear error message

We likely have to add proper explicit handling of universe levels. This has been the elephant in the room for a year. The downside is that the solver would have to be aware of it.

aniva pushed to game/touhou at aniva/OpenMusicScores 2024-06-10 11:53:01 -07:00
5dc9f82577 Merge branch 'main' into game/touhou
113fbb2cf4 Merge pull request 'Lemon (Yonezu Kenshi)' (#8) from misc/lemon into main
60b3ed9de6 Lemon finger position fix
5131965b2f Lemon remainder, articulation, and finger position
02715c34d4 Lemon (part 1)
Compare 5 commits »
aniva deleted branch misc/lemon from aniva/OpenMusicScores 2024-06-10 00:26:33 -07:00