 Leni Aniva
|
6d85c19589
|
feat: Add library bindings for calc
|
2024-04-11 15:04:36 -07:00 |
|
Leni Aniva
|
f02f9592d7
|
feat: Focus command
|
2024-04-08 13:12:51 -07:00 |
|
Leni Aniva
|
0e63583a1d
|
refactor: Monads in library
|
2024-04-08 12:54:02 -07:00 |
|
Leni Aniva
|
d4e49310f0
|
feat: FFI interface to conv functions
|
2024-04-08 12:50:41 -07:00 |
|
Leni Aniva
|
38cb91652f
|
Merge branch 'dev' into goal/have-conv-calc
|
2024-04-06 22:04:52 -07:00 |
|
Leni Aniva
|
5a60ca74d5
|
fix: Auto bound implicit in elab
|
2024-04-06 17:45:36 -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
|
8b43dc0f25
|
feat: Instantiate mvars during echo
|
2024-03-31 17:09:24 -07:00 |
|
Leni Aniva
|
744c9ee286
|
Merge pull request 'feat: Specify type in echo' (#55) from expr/echo into dev
Reviewed-on: #55
|
2024-03-31 16:45:43 -07:00 |
|
Leni Aniva
|
a1ed8f4b3d
|
refactor: Use library functions when possible
|
2024-03-31 16:11:41 -07:00 |
|
Leni Aniva
|
7988a25ce8
|
refactor: Use library goalStartExpr function
|
2024-03-31 16:06:30 -07:00 |
|
Leni Aniva
|
2802cc204f
|
feat: Specify type in echo
|
2024-03-31 15:55:08 -07:00 |
|
Leni Aniva
|
2b71203c1e
|
fix: Instantiation causes infinite loop
|
2024-03-30 00:17:16 -07:00 |
|
Leni Aniva
|
252f85e66c
|
feat: Instantiation tests
Note that delay assigned metavariables are not instantiated.
|
2024-03-29 23:46:08 -07:00 |
|
Leni Aniva
|
8fa1a7d383
|
feat: Stop cataloging internal/detail dependencies
|
2024-03-28 19:49:44 -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
|
3debcc021a
|
feat(lib): Export goal.print function
|
2024-03-14 16:34:01 -07:00 |
|
Leni Aniva
|
4eec930dd4
|
fix: Pass options by reference
|
2024-03-11 21:31:59 -07:00 |
|
Leni Aniva
|
ef864ea16d
|
feat(lib): Option creation function
|
2024-03-10 15:33:32 -07:00 |
|
Leni Aniva
|
0b91c41ad2
|
fix: Execute expr parsing within goal.start
|
2024-03-10 15:09:38 -07:00 |
|
Leni Aniva
|
a5b0721482
|
feat(lib): Expose goal state interface
|
2024-03-10 08:13:10 -07:00 |
|
Leni Aniva
|
996f16bbb8
|
feat(lib): CoreM execution function
|
2024-03-10 06:41:35 -07:00 |
|
Leni Aniva
|
f18a9dd1d5
|
refactor: Move some functions to `Library.lean`
|
2024-03-09 20:37:48 -08:00 |
|
Leni Aniva
|
eeb149a32c
|
feat(lib): Search path function
|
2024-03-09 19:36:25 -08:00 |
|
Leni Aniva
|
2ad7ad8778
|
feat(lib): Catalog command FFI
|
2024-03-09 16:50:36 -08:00 |
|
Leni Aniva
|
7bc0f82654
|
feat: Add exported version function
|
2024-03-08 23:50:44 -08:00 |