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
13
 Projects Packages Public Activity Starred Repositories
9
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 pushed to chore/version at aniva/Pantograph 2024-12-09 20:18:04 -08:00
e9cbc6eab3 chore: Update version
aniva created branch chore/version in aniva/Pantograph 2024-12-09 20:18:04 -08:00
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
aniva commented on pull request aniva/Pantograph#139 2024-12-09 17:22:00 -08:00
fix: Tactic failure on synthesizing placeholder

Adding this snippet to GoalState.tryTacticM fixes the test

    let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar goal)

    if (← Elab.Term.logUnassignedUsingErrorIn…
aniva created pull request aniva/Pantograph#139 2024-12-09 08:15:54 -08:00
fix: Tactic failure on synthesizing placeholder
aniva created branch bug/tactic-failure-placeholder in aniva/Pantograph 2024-12-09 08:15:26 -08:00
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-09 08:15:26 -08:00
7fc2bd0d0f test: Tactic failure on synthesizing placeholder
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-09 00:06:32 -08:00
2d068ecd50 fix: Use guarded `isDefEq`
17ab2eafd8 fix: Halt on match guard
Compare 2 commits »