aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 6 Pull Requests 2 Packages Projects Releases 1 Wiki Activity
145 Commits 7 Branches 14 Tags 1 MiB
Commit Graph

26 Commits

Author SHA1 Message Date
Leni Aniva 5720c72515
feat: Prevent crash during rootExpr call 2024-01-30 17:22:20 -08:00
Leni Aniva 9a5ee49778
feat: Print parent expression assignment 2024-01-24 18:19:04 -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 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