Leni Aniva

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 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 closed issue aniva/Pantograph#114

2024-12-08 16:25:24 -08:00

Incremental and intercepted parsing of Lean code

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

aniva pushed to frontend/infotree at aniva/Pantograph

2024-12-08 12:54:27 -08:00

4de53e0547 Merge branch 'dev' into frontend/infotree

d7457cd386 Merge pull request 'fix: Capture nested tactic failure' (#135) from bug/nested-tactic-failure into dev

929311a042 fix: Only signal failure when there is error

0415baaaff chore: Cleanup old `TestM`

34a4bf5b73 feat: Export GoalState.tryTactic

Compare 27 commits »

aniva pushed to dev at aniva/Pantograph

2024-12-07 18:51:28 -08:00

d7457cd386 Merge pull request 'fix: Capture nested tactic failure' (#135) from bug/nested-tactic-failure into dev

929311a042 fix: Only signal failure when there is error

0415baaaff chore: Cleanup old `TestM`

34a4bf5b73 feat: Export GoalState.tryTactic

a62ac51c37 chore: Remove all redundant filenames

Compare 7 commits »

aniva deleted branch bug/nested-tactic-failure from aniva/Pantograph

2024-12-07 18:51:28 -08:00

aniva merged pull request aniva/Pantograph#135

2024-12-07 18:51:26 -08:00

fix: Capture nested tactic failure

aniva pushed to tool/lighting at aniva/Cosplay

2024-12-07 13:47:39 -08:00

6470010da6 fix: Model name

5ab611666e Merge branch 'lib/build' into tool/lighting

a6685e6779 feat: Add model name prefix to build path

418e6517a0 fix: Sketch object attribute

Compare 4 commits »

aniva created pull request aniva/Cosplay#10

2024-12-07 13:46:59 -08:00

feat: Add model name prefix to build path