Leni Aniva
ab1b309c72
feat: Use CoreM as the main interaction monad
2023-12-12 18:39:02 -08:00
Leni Aniva
c76751861a
fix: Change the main interaction monad to MetaM
2023-12-08 16:17:16 -08:00
Leni Aniva
7c28cf4ed0
Merge branch 'dev' into goal/continuation
2023-11-06 11:45:24 -08:00
Leni Aniva
c5f563598d
chore: Remove unnecessary unsafe's
2023-11-06 11:43:57 -08:00
Leni Aniva
dbace9f2d5
fix: Use Lean's built in name parser
...
The `str_to_name` parser cannot handle numerical names and escapes.
2023-11-06 10:45:11 -08:00
Leni Aniva
9447d29e37
Store states instead of goals
...
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)
Documentations pending
2023-10-15 17:15:23 -07:00
Leni Aniva
836a14fa63
Bump Lean version to 4.1.0
2023-10-05 17:49:43 -07:00
Leni Aniva
8e02e6e7cc
Add ready message to indicate the main loop is up
2023-10-02 10:14:03 -07:00
Leni Aniva
7160f8aa61
Merge branch 'dev' into io/serial
2023-08-23 13:25:08 -07:00
Leni Aniva
85440e0278
Unify json and unknown error into command error
2023-08-23 13:00:11 -07:00
Leni Aniva
1d1fa60175
Move all json-string functions to Main.lean
2023-08-22 09:54:37 -07:00
Leni Aniva
ddf7ec21c8
Add compressed json print option; Rearrange commands into hierarchy
2023-08-16 19:25:32 -07:00
Leni Aniva
0e61093f47
Add proof variable delta; Bump version to 0.2.1
2023-08-15 15:40:54 -07:00
Leni Aniva
19c57ada1e
Add expression sexp printing (1/2, tests pending)
2023-08-14 17:07:53 -07:00
Leni Aniva
d705cdf0e5
version bump, restructure
2023-08-13 21:19:06 -07:00
Leni Aniva
a00a2b4a42
Add documentation; Remove mathlib dependency
2023-06-09 14:45:45 -07:00
Leni Aniva
572548c1bd
Add json goal printing
2023-05-27 23:10:39 -07:00
Leni Aniva
9fe3f62371
Add back the clear command to reset state
2023-05-26 16:55:33 -07:00
Leni Aniva
989130ecd2
Add expr.type
2023-05-25 13:40:03 -07:00
Leni Aniva
5beb911db5
Rename tactic failure mode to avoid confusion
...
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva
fd536da55c
Add expression binding printing and import Lean
2023-05-24 00:54:48 -07:00
Leni Aniva
58367cef6c
Use TermElabM as the main monad stack instead of IO
2023-05-23 05:12:46 -07:00
Leni Aniva
c781797898
Save core state in proofs
2023-05-22 22:48:48 -07:00
Leni Aniva
44d470d63e
Rename ids so they are consistent
2023-05-22 19:51:16 -07:00
Leni Aniva
56b967ee7a
Add module name for symbol
2023-05-22 16:00:41 -07:00
Leni Aniva
22202af24e
Add option id handling with ?
2023-05-22 14:56:43 -07:00
Leni Aniva
111dea2093
Add option format for proof output and test cases
2023-05-22 14:49:56 -07:00
Leni Aniva
2772a394cc
Add default arguments for Json
2023-05-22 00:49:37 -07:00
Leni Aniva
41241bfa40
Add REPL tactics
2023-05-21 17:41:39 -07:00
Leni Aniva
ed70875837
Remove ExceptT from main monad
...
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva
c4a1ccad13
Add expression IO stub for constant types
2023-05-20 14:04:09 -07:00
Leni Aniva
65da39440d
Add alternative command input format and IO stub
2023-05-20 13:03:12 -07:00
14a6eb1f59
Add tactic state manipulation
2023-05-17 21:58:03 -07:00
2ec4efde55
Add stack size troubleshooting
2023-05-14 15:22:41 -07:00
3cb0795bb6
Add unsafe filtering in catalog
2023-05-12 16:12:21 -07:00
Leni Aniva
9f53781ffe
Add working catalog code and example
2023-05-12 01:08:36 -07:00
5a297e8fef
Add README and catalog functions
2023-05-09 22:51:19 -07:00
Leni Aniva
0b2db92b4a
Separate commands into its own file
2023-05-09 18:01:09 -07:00
9a957bce35
Add REPL
2023-05-09 16:39:24 -07:00
Leni Aniva
9bba78eb1d
Initial commit
2023-05-07 15:19:45 -07:00
Leni Aniva
Leni Ven