Leni Aniva
6b44d9ef14
fix: Remove `calcPrevRhs?` in non-calc tactics
2024-04-11 15:03:14 -07:00
Leni Aniva
535770bbd7
feat: Calc tactic
2024-04-11 14:59:55 -07:00
Leni Aniva
30c1fd894f
fix: Coupling from unrelated goals
2024-04-09 09:11:15 -07:00
Leni Aniva
f02f9592d7
feat: Focus command
2024-04-08 13:12:51 -07:00
Leni Aniva
2f48cfbc19
doc: Remove outdated comments
2024-04-08 12:45:03 -07:00
Leni Aniva
22bb818a1c
refactor: Use the `tactic interface for `conv
2024-04-08 12:32:27 -07:00
Leni Aniva
63e64a1e9f
feat: Conv tactic functions
2024-04-08 12:26:22 -07:00
Leni Aniva
19d2f5ff3f
feat: Conv tactic mode
2024-04-07 17:03:49 -07:00
Leni Aniva
d50720f622
refactor: Metavariable set diff function
2024-04-07 14:32:25 -07:00
Leni Aniva
d9ed051b4d
feat: Partial implementation of `conv`
2024-04-07 14:22:20 -07:00
Leni Aniva
7fe73551c3
feat: The `have` tactic
2024-04-06 21:52:25 -07:00
Leni Aniva
058f5a98b2
feat: Bindings for the `have` tactic
2024-04-06 16:40:22 -07:00
Leni Aniva
1b7b6a644b
feat: `GoalState.tryHave` tactic (tests failing)
2024-04-06 16:33:20 -07:00
Leni Aniva
7e28ded23f
test: More diagnostics for tests
2024-03-06 15:14:08 -08:00
Leni Aniva
fe5c1eda7d
feat: Prevent crash during rootExpr call
2024-01-30 17:22:20 -08:00
Leni Aniva
25f3a2f19d
feat: Print parent expression assignment
2024-01-24 18:19:04 -08:00
Leni Aniva
dc90b6b73e
chore: Move environment functions to its own file
...
Symbol.lean is now subsumed
2023-12-15 13:40:36 -05:00
Leni Aniva
bd0c66facc
fix: Consolidate TermElabM blocks
2023-12-08 17:31:25 -08:00
Leni Aniva
4be9dbc84a
feat: Goal continuation fails if target has goals
2023-11-04 15:53:57 -07:00
Leni Aniva
333355a85d
feat: Partial state continuation
2023-11-04 15:33:53 -07:00
Leni Aniva
4a4a33cea7
test: Separate mvar coupling tests
2023-11-04 15:01:41 -07:00
Leni Aniva
045181356c
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
f064bb21a4
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
269e5c707c
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
c852db2f46
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
8029298db7
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
d991533170
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07:00
Leni Aniva
538ba6e7d7
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
41db295ff5
Rename tactic to goal and restructure
2023-10-15 12:31:22 -07:00
Leni Aniva