Enable handling of m-Coupled goals #20

Merged

aniva merged 11 commits from goal/dependency into dev

2023-10-27 19:30:21 -07:00

Author	SHA1	Message	Date
Leni Aniva	427d819349	feat: Add REPL function for root expression	2023-10-27 15:41:12 -07:00
Leni Aniva	ca7a081cac	Merge branch 'dev' into goal/dependency	2023-10-27 15:33:47 -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	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