Leni Aniva

aniva pushed to bug/incorrect-binder-capture at aniva/Pantograph

2024-12-21 15:57:23 -08:00

80f9aa3269 merge: branch 'misc/version' into bug/incorrect-binder-capture

5a05e9e8d4 test: Add binder capturing test

48b924fae2 fix(frontend): Incorrect capture of binder term

Compare 3 commits »

aniva created branch bug/incorrect-binder-capture in aniva/Pantograph

2024-12-21 15:57:23 -08:00

aniva opened issue aniva/Pantograph#151

2024-12-19 05:02:52 -08:00

Add unsafe detection in goal.print

aniva opened issue aniva/Pantograph#150

2024-12-19 05:02:20 -08:00

Allow LSP-like behaviour of finding definition location via symbol

aniva created pull request aniva/Pantograph#149

2024-12-16 15:21:38 -08:00

feat: Simplify sexp printing

aniva created pull request aniva/Pantograph#148

2024-12-16 15:19:47 -08:00

fix: Unnecessary instantiation call

aniva pushed to goal/tactic at aniva/Pantograph

2024-12-16 15:18:43 -08:00

b42d917aa7 fix: Unnecessary instantiation call

3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev

0fa57a5a15 Merge branch 'dev' into goal/print

b9c114fe21 Merge pull request 'doc: Add limitations' (#145) from doc/rationale into dev

2f732a7f20 feat: Print goals in `goal.print`

Compare 131 commits »

aniva created branch delate/sexp in aniva/Pantograph

2024-12-16 15:18:02 -08:00

aniva pushed to delate/sexp at aniva/Pantograph

2024-12-16 15:18:02 -08:00

53bad1c4c9 refactor: Remove obsolete sanitize option

7a3b89cc0e feat: Simplify sexp binder

c0090dec97 fix: Quote string literal in sexp

Compare 3 commits »

aniva opened issue aniva/Pantograph#147

2024-12-14 18:43:51 -08:00

Separate tactics list from this library

aniva commented on pull request aniva/Pantograph#134

2024-12-11 20:59:20 -08:00

chore: Update Lean to v4.14.0

test_tactic_failure_synthesize_placeholder is failing, and this is due to changing behaviour in Lean's tactic execution system. Previously "don't know how to synthesize placeholder" is something…

aniva pushed to misc/version at aniva/Pantograph

2024-12-11 20:53:40 -08:00

13e01b9e62 Merge branch 'dev' into misc/version

3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev

0fa57a5a15 Merge branch 'dev' into goal/print

b9c114fe21 Merge pull request 'doc: Add limitations' (#145) from doc/rationale into dev

2f732a7f20 feat: Print goals in `goal.print`

Compare 52 commits »

aniva closed issue aniva/Pantograph#131

2024-12-11 18:24:24 -08:00

Add aarch64-{linux,darwin} targets in flake

aniva commented on issue aniva/Pantograph#131

2024-12-11 18:24:17 -08:00

Add aarch64-{linux,darwin} targets in flake

Done #143

aniva pushed tag v0.2.23 to aniva/Pantograph

2024-12-11 17:01:19 -08:00

aniva deleted branch goal/print from aniva/Pantograph

2024-12-11 16:52:23 -08:00

aniva pushed to dev at aniva/Pantograph

2024-12-11 16:52:22 -08:00

3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141) from goal/print into dev

0fa57a5a15 Merge branch 'dev' into goal/print

2f732a7f20 feat: Print goals in `goal.print`

eeb336c944 Merge branch 'dev' into goal/print

0725d865de feat: Print value of arbitrary mvar in goal state

Compare 5 commits »

aniva merged pull request aniva/Pantograph#141

2024-12-11 16:52:21 -08:00

feat: Print value of arbitrary mvar and goals in goal state

aniva closed issue aniva/Pantograph#138

2024-12-11 16:52:21 -08:00

Articulation of Finished Proof

aniva pushed to goal/print at aniva/Pantograph

2024-12-11 16:52:07 -08:00

0fa57a5a15 Merge branch 'dev' into goal/print

b9c114fe21 Merge pull request 'doc: Add limitations' (#145) from doc/rationale into dev

bb445f4d73 chore: Update version

f111da7de7 doc: Add limitations

fecab387dc merge: branch 'dev' into doc/rationale

Compare 5 commits »