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 merged pull request aniva/Pantograph#149 2025-01-07 17:31:30 -08:00
feat: Simplify sexp printing
aniva pushed to dev at aniva/Pantograph 2025-01-07 17:31:10 -08:00
56f40462ae Merge pull request 'fix: Unnecessary instantiation call' (#148) from goal/tactic into dev
b42d917aa7 fix: Unnecessary instantiation call
Compare 2 commits »
aniva deleted branch goal/tactic from aniva/Pantograph 2025-01-07 17:31:10 -08:00
aniva merged pull request aniva/Pantograph#148 2025-01-07 17:31:09 -08:00
fix: Unnecessary instantiation call
aniva created pull request aniva/Pantograph#152 2025-01-07 17:25:47 -08:00
fix: Incorrect binder capture
aniva pushed to bug/incorrect-binder-capture at aniva/Pantograph 2025-01-07 17:24:24 -08:00
524314721b feat: Gate type error collection behind flag
aniva created branch bug/incorrect-binder-capture in aniva/Pantograph 2024-12-21 15:57:23 -08:00
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 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.15.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