Leni Aniva aniva
  • Stanford University Centaur Lab
  • https://leni.sh
  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
aniva deleted branch doc from aniva/Pantograph 2024-04-11 15:45:26 -07:00
aniva closed pull request aniva/Pantograph#28 2024-04-11 15:45:01 -07:00
WIP: Proof tracing from theorem library
aniva deleted branch library/trace from aniva/Pantograph 2024-04-11 15:45:01 -07:00
aniva pushed to main at aniva/Pantograph 2024-04-11 15:44:03 -07:00
622aa7f969 Add documentation; Remove mathlib dependency
4613777607 Add json goal printing
3e05722d1e Add back the clear command to reset state
068a188fea Add expr.type
e0c5f76451 Rename tactic failure mode to avoid confusion
Compare 29 commits »
aniva pushed to library/trace at aniva/Pantograph 2024-04-11 15:44:02 -07:00
1638c308a9 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev
59ac83f0b7 bug: Fix quote escape problem
d1c0dc376f feat: Print metavariable name in goal
6cf328a84f Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
1a99a2e7b2 fix: Sanitize name in universe levels
Compare 79 commits »
aniva pushed to doc at aniva/Pantograph 2024-04-11 15:44:02 -07:00
bd4fbcc369 Add test cases for command error categories
ff8fed8741 Classify JSON error as command error
98edaa3297 Merge pull request 'Add more serialisation options' (#2) from io/serial into dev
1f27532769 Merge branch 'dev' into io/serial
0c330c8778 Unify json and unknown error into command error
Compare 41 commits »
aniva pushed to dev at aniva/Pantograph 2024-04-11 15:44:02 -07:00
f20ee8dc87 Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59) from goal/have-conv-calc into dev
a41b95e540 Merge branch 'dev' into goal/have-conv-calc
a11df9f2e9 feat: Print recursor rules
ed220bc7fb doc: New tactics in README.md
7eb5419f36 feat: REPL interface for `calc`
Compare 230 commits »
aniva pushed to dev at aniva/Pantograph 2024-04-11 15:36:20 -07:00
2e9fc313ad Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59) from goal/have-conv-calc into dev
440cc1c920 Merge branch 'dev' into goal/have-conv-calc
db35ec7187 doc: New tactics in README.md
327b402cdf feat: REPL interface for `calc`
222cb035d1 feat: Add library bindings for calc
Compare 23 commits »
aniva deleted branch goal/have-conv-calc from aniva/Pantograph 2024-04-11 15:36:20 -07:00
aniva merged pull request aniva/Pantograph#59 2024-04-11 15:36:20 -07:00
feat: Add support for the `have`, `conv`, and `calc` tactics
aniva pushed to goal/have-conv-calc at aniva/Pantograph 2024-04-11 15:36:03 -07:00
440cc1c920 Merge branch 'dev' into goal/have-conv-calc
e43601de4b feat: Print recursor rules
56cfe523df fix: Leading element in .proj sexp
9cc770c3c9 fix: Serialization of .proj
Compare 4 commits »
aniva pushed to dev at aniva/Pantograph 2024-04-11 15:35:16 -07:00
e43601de4b feat: Print recursor rules
aniva deleted branch env/inspect from aniva/Pantograph 2024-04-11 15:35:16 -07:00
aniva merged pull request aniva/Pantograph#65 2024-04-11 15:35:15 -07:00
feat: Print precursor rules in env/inspect
aniva pushed to goal/have-conv-calc at aniva/Pantograph 2024-04-11 15:13:22 -07:00
db35ec7187 doc: New tactics in README.md
327b402cdf feat: REPL interface for `calc`
Compare 2 commits »
aniva pushed to goal/have-conv-calc at aniva/Pantograph 2024-04-11 15:04:45 -07:00
222cb035d1 feat: Add library bindings for calc
663651b10e fix: Remove `calcPrevRhs?` in non-calc tactics
Compare 2 commits »
aniva pushed to goal/have-conv-calc at aniva/Pantograph 2024-04-11 15:00:06 -07:00
403d92692e feat: Calc tactic
aniva created pull request aniva/Pantograph#65 2024-04-11 12:39:36 -07:00
feat: Print precursor rules in env/inspect
aniva pushed to env/inspect at aniva/Pantograph 2024-04-09 21:29:24 -07:00
a1599e6016 Merge branch 'dev' into env/inspect
56cfe523df fix: Leading element in .proj sexp
9cc770c3c9 fix: Serialization of .proj
Compare 3 commits »
aniva pushed to env/inspect at aniva/Pantograph 2024-04-09 21:29:09 -07:00
8198fe5424 feat: Print recursor rules
c629163aa1 perf: Lazy run print monads
be44eadde5 Merge pull request 'fix: Auto bound implicit in elab' (#60) from elab/level into dev
d72a60f4e4 fix: Auto bound implicit in elab
d44693e548 doc: Documentation for `nix flake check`
Compare 15 commits »