Leni Aniva
e2526f11b1
feat: Print names in one segment separated with .
2023-10-29 11:56:56 -07:00
Leni Aniva
c2d606b9d9
feat: Simplify name printing
2023-10-29 11:18:35 -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
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
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
e63f7c9afa
Add proper printing of sorts
2023-08-23 12:51:06 -07:00
Leni Aniva
d476354a4a
Add expression sexp printing (2/2)
2023-08-14 21:43:40 -07:00
Leni Aniva
fd536da55c
Add expression binding printing and import Lean
2023-05-24 00:54:48 -07:00
Leni Aniva
111dea2093
Add option format for proof output and test cases
2023-05-22 14:49:56 -07:00
Leni Aniva