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 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 »
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-08 23:22:08 -08:00
ea813e5bc5 feat: Monadic info collection
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-08 22:52:13 -08:00
b950dc9b1a fix: Verbose printing of infotree
aniva pushed to game/touhou/04-bad-apple at aniva/OpenMusicScores 2024-12-08 16:59:55 -08:00
6814f79b95 Finger positions for Bad Apple!!
aniva closed issue aniva/Pantograph#114 2024-12-08 16:25:24 -08:00
Incremental and intercepted parsing of Lean code
aniva commented on issue aniva/Pantograph#114 2024-12-08 16:25:24 -08:00
Incremental and intercepted parsing of Lean code

Superseded by specific frontend functions.

aniva opened issue aniva/Pantograph#138 2024-12-08 16:25:02 -08:00
Directly pretty-print finished goals to Lean text
aniva opened issue aniva/Pantograph#137 2024-12-08 16:11:48 -08:00
Pickle environment extensions
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-08 15:38:16 -08:00
9ede3cf717 feat: InfoTree printing
aniva created pull request aniva/Pantograph#136 2024-12-08 12:55:42 -08:00
chore: Version 0.3