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 goal/print in aniva/Pantograph 2024-12-10 12:40:48 -08:00
aniva pushed to goal/print at aniva/Pantograph 2024-12-10 12:40:48 -08:00
ff49a64a13 feat: Dump proof expressions of arbitrary mvars
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-10 12:22:11 -08:00
681c3fb78d fix: Disallow indeterminant type `sorry`
aniva commented on pull request aniva/Pantograph#139 2024-12-09 21:44:59 -08:00
fix: Tactic failure on synthesizing placeholder

Should be ready to go

aniva pushed to dev at aniva/Pantograph 2024-12-09 21:43:05 -08:00
e9cbc6eab3 chore: Update version
aniva deleted branch chore/version from aniva/Pantograph 2024-12-09 21:43:05 -08:00
aniva merged pull request aniva/Pantograph#140 2024-12-09 21:43:04 -08:00
chore: Update version
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 21:40:10 -08:00
37a5884be4 fix: Use `ppSyntax` instead of `ppTactic`
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 21:00:51 -08:00
1527743900 refactor: Optionalize CompilationUnit
eb0374dfb3 feat: Collect new constants in repl
Compare 2 commits »
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 20:42:13 -08:00
9a69c48cb2 fix: Integration test failure
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 20:38:46 -08:00
dd00d803d1 feat: Collect sorry/elab failure boundaries
aniva created pull request aniva/Pantograph#140 2024-12-09 20:18:18 -08:00
chore: Update version
aniva created branch chore/version in aniva/Pantograph 2024-12-09 20:18:04 -08:00
aniva pushed to chore/version at aniva/Pantograph 2024-12-09 20:18:04 -08:00
e9cbc6eab3 chore: Update version
aniva commented on pull request aniva/Pantograph#128 2024-12-09 20:16:24 -08:00
feat: Extract type error and new constants

Ready to go.

aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 20:16:19 -08:00
0b4ded1049 fix: Collect sorrys and type mismatches
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 19:40:20 -08:00
5ef2b5c118 feat: Collect newly defined constants
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-09 17:58:31 -08:00
d040d2006c fix: Do not guard mvar errors in other tactics
aniva commented on pull request aniva/Pantograph#139 2024-12-09 17:34:54 -08:00
fix: Tactic failure on synthesizing placeholder

Introduced regression. Waiting on decision of issue author to pick a solution.

aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-09 17:30:55 -08:00
47d26badc8 feat: Capture mvar errors