feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00

22 Commits

Author SHA1 Message Date
Leni Aniva 440cc1c920
Merge branch 'dev' into goal/have-conv-calc 2024-04-11 15:35:30 -07:00
Leni Aniva db35ec7187
doc: New tactics in README.md 2024-04-11 15:13:12 -07:00
Leni Aniva 327b402cdf
feat: REPL interface for `calc` 2024-04-11 15:11:10 -07:00
Leni Aniva 222cb035d1
feat: Add library bindings for calc 2024-04-11 15:04:36 -07:00
Leni Aniva 663651b10e
fix: Remove `calcPrevRhs?` in non-calc tactics 2024-04-11 15:03:14 -07:00
Leni Aniva 403d92692e
feat: Calc tactic 2024-04-11 14:59:55 -07:00
Leni Aniva 100cdd885f
fix: Coupling from unrelated goals 2024-04-09 09:11:15 -07:00
Leni Aniva 9a04fd4819
feat: Focus command 2024-04-08 13:12:51 -07:00
Leni Aniva dd94e29293
refactor: Monads in library 2024-04-08 12:54:02 -07:00
Leni Aniva 9fbc65829d
feat: FFI interface to conv functions 2024-04-08 12:50:41 -07:00
Leni Aniva f3a3ca31a0
doc: Remove outdated comments 2024-04-08 12:45:03 -07:00
Leni Aniva 73bdcb6be6
refactor: Use the `tactic interface for `conv 2024-04-08 12:32:27 -07:00
Leni Aniva 3094d11e48
feat: Conv tactic functions 2024-04-08 12:26:22 -07:00
Leni Aniva ea0f411949
Merge branch 'dev' into goal/have-conv-calc 2024-04-08 10:38:18 -07:00
Leni Aniva ab0d87450a
feat: Conv tactic mode 2024-04-07 17:03:49 -07:00
Leni Aniva aba1d9be10
refactor: Metavariable set diff function 2024-04-07 14:32:25 -07:00
Leni Aniva 9d7c9598f5
feat: Partial implementation of `conv` 2024-04-07 14:22:20 -07:00
Leni Aniva 5925b6163a
Merge branch 'dev' into goal/have-conv-calc 2024-04-06 22:04:52 -07:00
Leni Aniva aa8da3014e
feat: The `have` tactic 2024-04-06 21:52:25 -07:00
Leni Aniva 3db1207aa6
test: Tests for conv and calc 2024-04-06 17:22:09 -07:00
Leni Aniva 951c2cec19
feat: Bindings for the `have` tactic 2024-04-06 16:40:22 -07:00
Leni Aniva ace2ddf478
feat: `GoalState.tryHave` tactic (tests failing) 2024-04-06 16:33:20 -07:00