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
754fb69cff
feat: Partial state continuation
2023-11-04 15:33:53 -07:00
Leni Aniva
dc2cc5be77
test: Separate mvar coupling tests
2023-11-04 15:01:41 -07:00
Leni Aniva
d87217c6bb
feat: Print metavariable name in goal
2023-10-30 14:44:06 -07:00
Leni Aniva
427d819349
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
b381d89ff9
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
e98fb77f33
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
4ffd226cac
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
0ecfa9fc26
feat: Display user name in Goal structure
...
1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression
2023-10-25 22:18:59 -07:00
Leni Aniva
0a0f0304a8
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07: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
8c93d30ab7
Rename tactic to goal and restructure
2023-10-15 12:31:22 -07:00
Leni Aniva
42133f9b74
Add holes test stub
...
Move tests into their own namespaces
2023-10-06 17:31:36 -07:00
Leni Aniva
5b002a9ceb
Fix test failures
2023-10-05 17:51:41 -07:00
Leni Aniva
0c5f439067
Add SemihashMap structure for goal bookkeeping
2023-08-27 19:53:09 -07:00
Leni Aniva
81702d12ef
Remove the obsolete name field from proof tree structure
2023-08-26 18:50:15 -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
d476354a4a
Add expression sexp printing (2/2)
2023-08-14 21:43:40 -07:00
Leni Aniva
572548c1bd
Add json goal printing
2023-05-27 23:10:39 -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
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