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 |