- Stanford University Centaur Group
- https://leni.sh
-
Admin of this website
- Joined on
2023-08-21
Add support for
have
, conv
, calc
, tactics.
fix: Prevent incorrectly inheritance of calc rhs
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
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
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
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`
feat: Add support for the `have`, `conv`, and `calc` tactics
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
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