- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
WIP: Proof tracing from theorem library
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
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
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
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`
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
feat: Add support for the `have`, `conv`, and `calc` tactics
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
feat: Print precursor rules in env/inspect
db35ec7187
doc: New tactics in README.md
327b402cdf
feat: REPL interface for `calc`
222cb035d1
feat: Add library bindings for calc
663651b10e
fix: Remove `calcPrevRhs?` in non-calc tactics
feat: Print precursor rules in env/inspect
a1599e6016
Merge branch 'dev' into env/inspect
56cfe523df
fix: Leading element in .proj sexp
9cc770c3c9
fix: Serialization of .proj
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`