aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 3 Packages Projects Releases Wiki Activity
140 Commits 5 Branches 26 Tags 1.8 MiB
Commit Graph

22 Commits

Author SHA1 Message Date
Leni Aniva 79b6974172
Merge branch 'dev' into goal/diag 2024-01-17 14:03:19 -08:00
Leni Aniva efa956464d
test: Option controlled mvar instantiation 2024-01-16 16:44:54 -08:00
Leni Aniva 93a34f9fda
feat: Print constructor and recursor info 2024-01-16 14:11:52 -08:00
Leni Aniva a1421439f8
feat: Print inductives in env.inspect 2024-01-16 13:29:30 -08:00
Leni Aniva aca7dc9811
refactor: env. operations into its own file 2023-12-15 13:37:55 -05:00
Leni Aniva 02889510b2
feat: env_add command 2023-12-13 19:35:32 -08:00
Leni Aniva 12544b81ee
chore: Rename lib. commands to env. 
This is done to improve clarity and align with Lean's terminology
 2023-12-12 18:56:25 -08:00
Leni Aniva ccf5a03647
fix: Printing projection leads to crash 2023-12-05 22:45:59 -08:00
Leni Aniva da74258dd1
feat!: Display public name only if name is private 2023-12-05 20:20:08 -08:00
Leni Aniva 9f2b07757f
feat: Display whether a symbol is private 2023-12-05 19:07:00 -08:00
Leni Aniva 7b59937853
feat: Read dependencies of library symbols 2023-11-25 15:07:56 -08:00
Leni Aniva 2a9931c134
fix: Rectify error format 2023-11-09 22:24:17 -08:00
Leni Aniva 245e76b2f1
feat: Print the root mvar name 2023-11-06 11:51:31 -08:00
Leni Aniva db706070ad
feat: Add goal.continue command 2023-11-04 15:51:09 -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 82f5494718
feat: Add REPL command for assigning an expression 2023-10-27 15:32:59 -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 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