 Leni Aniva
|
431ca4e481
|
fix: Move elab context to condensed
|
2024-07-22 17:57:01 -07:00 |
|
Leni Aniva
|
ffbea41f62
|
feat: Condensed interface
|
2024-06-25 15:13:58 -04:00 |
|
Leni Aniva
|
92acf7782c
|
test: CongruenceArg tactic
|
2024-05-20 11:51:35 -07:00 |
|
Leni Aniva
|
3812aa56ec
|
feat: Phantom var in mapply
|
2024-04-22 00:11:41 -07:00 |
|
Leni Aniva
|
dbd54f7679
|
feat: Implement the mapply tactic
|
2024-04-15 12:47:02 -07:00 |
|
Leni Aniva
|
63e64a1e9f
|
feat: Conv tactic functions
|
2024-04-08 12:26:22 -07:00 |
|
Leni Aniva
|
5a60ca74d5
|
fix: Auto bound implicit in elab
|
2024-04-06 17:45:36 -07:00 |
|
Leni Aniva
|
92351c9a3d
|
test: Move parallelism to Test/Main.lean
|
2024-04-06 14:14:30 -07:00 |
|
Leni Aniva
|
8a447e67cd
|
test: Parallel testing infrastructure
|
2024-04-06 14:07:13 -07:00 |
|
Leni Aniva
|
216bb9e920
|
test: Library test
|
2024-03-31 16:43:30 -07:00 |
|
Leni Aniva
|
a698a4250f
|
feat: Unfold aux lemmas when printing root expr
|
2024-03-28 18:56:42 -07:00 |
|
Leni Aniva
|
516ab15961
|
feat: Bump toolchain version
|
2024-03-28 00:06:35 -07:00 |
|
Leni Aniva
|
6692303da6
|
test: Simplify monad execution
|
2024-01-07 14:14:20 -08:00 |
|
Leni Aniva
|
4a4a33cea7
|
test: Separate mvar coupling tests
|
2023-11-04 15:01:41 -07:00 |
|
Leni Aniva
|
d1c0dc376f
|
feat: Print metavariable name in goal
|
2023-10-30 14:44:06 -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 |