Leni Aniva
eeb149a32c
feat(lib): Search path function
2024-03-09 19:36:25 -08:00
Leni Aniva
2ad7ad8778
feat(lib): Catalog command FFI
2024-03-09 16:50:36 -08:00
Leni Aniva
085b12c255
feat: Use CoreM as the main interaction monad
2023-12-12 18:39:02 -08:00
Leni Aniva
2fe4fa9bc4
fix: Change the main interaction monad to MetaM
2023-12-08 16:17:16 -08:00
Leni Aniva
32fedede6a
Merge branch 'dev' into goal/continuation
2023-11-06 11:45:24 -08:00
Leni Aniva
8182da436d
chore: Remove unnecessary unsafe's
2023-11-06 11:43:57 -08:00
Leni Aniva
ce1cb13e54
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
538ba6e7d7
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
a8cf94ccb1
Bump Lean version to 4.1.0
2023-10-05 17:49:43 -07:00
Leni Aniva
35b391881e
Add ready message to indicate the main loop is up
2023-10-02 10:14:03 -07:00
Leni Aniva
1f27532769
Merge branch 'dev' into io/serial
2023-08-23 13:25:08 -07:00
Leni Aniva
0c330c8778
Unify json and unknown error into command error
2023-08-23 13:00:11 -07:00
Leni Aniva
a8cbb3be4f
Move all json-string functions to Main.lean
2023-08-22 09:54:37 -07:00
Leni Aniva
96cbbf2551
Add compressed json print option; Rearrange commands into hierarchy
2023-08-16 19:25:32 -07:00
Leni Aniva
b2ba26528d
Add proof variable delta; Bump version to 0.2.1
2023-08-15 15:40:54 -07:00
Leni Aniva
9eadd1d4d4
Add expression sexp printing (1/2, tests pending)
2023-08-14 17:07:53 -07:00
Leni Aniva
5cedb9d88c
version bump, restructure
2023-08-13 21:19:06 -07:00
Leni Aniva
622aa7f969
Add documentation; Remove mathlib dependency
2023-06-09 14:45:45 -07:00
Leni Aniva
4613777607
Add json goal printing
2023-05-27 23:10:39 -07:00
Leni Aniva
3e05722d1e
Add back the clear command to reset state
2023-05-26 16:55:33 -07:00
Leni Aniva
068a188fea
Add expr.type
2023-05-25 13:40:03 -07:00
Leni Aniva
e0c5f76451
Rename tactic failure mode to avoid confusion
...
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva
95ed7d115c
Add expression binding printing and import Lean
2023-05-24 00:54:48 -07:00
Leni Aniva
1fed222f56
Use TermElabM as the main monad stack instead of IO
2023-05-23 05:12:46 -07:00
Leni Aniva
94bc3355a2
Save core state in proofs
2023-05-22 22:48:48 -07:00
Leni Aniva
ba779766c0
Rename ids so they are consistent
2023-05-22 19:51:16 -07:00
Leni Aniva
0f8df08dd5
Add module name for symbol
2023-05-22 16:00:41 -07:00
Leni Aniva
116c7ff4c6
Add option id handling with ?
2023-05-22 14:56:43 -07:00
Leni Aniva
6a71dad389
Add option format for proof output and test cases
2023-05-22 14:49:56 -07:00
Leni Aniva
46ccad1669
Add default arguments for Json
2023-05-22 00:49:37 -07:00
Leni Aniva
083ec8beec
Add REPL tactics
2023-05-21 17:41:39 -07:00
Leni Aniva
15aab3d31f
Remove ExceptT from main monad
...
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva
2a4d348aab
Add expression IO stub for constant types
2023-05-20 14:04:09 -07:00
Leni Aniva
8127e9ba06
Add alternative command input format and IO stub
2023-05-20 13:03:12 -07:00
Leni Aniva
e246fd961f
Add tactic state manipulation
2023-05-17 21:58:03 -07:00
Leni Aniva
4d636ec12b
Add stack size troubleshooting
2023-05-14 15:22:41 -07:00
Leni Aniva
d3af535652
Add unsafe filtering in catalog
2023-05-12 16:12:21 -07:00
Leni Aniva
7c96479bb5
Add working catalog code and example
2023-05-12 01:08:36 -07:00
Leni Aniva
b5cb464694
Add README and catalog functions
2023-05-09 22:51:19 -07:00
Leni Aniva
f6a520c7a0
Separate commands into its own file
2023-05-09 18:01:09 -07:00
Leni Aniva
1a611c1415
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