Leni Aniva
|
a62ac51c37
|
chore: Remove all redundant filenames
|
2024-12-05 22:11:37 -08:00 |
Leni Aniva
|
82d99ccf9b
|
refactor: Use `MVarId` across the board
|
2024-09-06 21:07:12 -07:00 |
Leni Aniva
|
8d2cd6dfc7
|
fix: Bindings in prograde tactics
|
2024-09-03 14:15:52 -07:00 |
Leni Aniva
|
43e11f1ba3
|
refactor: Always display isInaccessible
|
2024-08-17 00:53:38 -07:00 |
Leni Aniva
|
e1b7eaab12
|
fix: Let tactic not bringing binder into scope
|
2024-08-17 00:47:12 -07:00 |
Leni Aniva
|
1e7a186bb1
|
refactor: MetaM form of define (evaluate)
|
2024-08-15 23:23:17 -07:00 |
Leni Aniva
|
6ddde2963d
|
test: Eval instantiate
|
2024-06-27 14:51:16 -04:00 |
Leni Aniva
|
fc0d872343
|
refactor: Simplify proof test infrastructure
|
2024-06-27 14:34:21 -04:00 |
Leni Aniva
|
58f9d72288
|
test: Evaluate tactic context
|
2024-06-25 16:18:31 -04:00 |
Leni Aniva
|
e282d9f781
|
test: Evaluation tactic
|
2024-06-25 11:03:08 -04:00 |