Leni Aniva
|
9cc770c3c9
|
fix: Serialization of .proj
|
2024-04-09 10:03:36 -07:00 |
Leni Aniva
|
d72a60f4e4
|
fix: Auto bound implicit in elab
|
2024-04-06 17:45:36 -07:00 |
Leni Aniva
|
fd47711e1f
|
test: Move parallelism to Test/Main.lean
|
2024-04-06 14:14:30 -07:00 |
Leni Aniva
|
4cbfc45292
|
test: Parallel testing infrastructure
|
2024-04-06 14:07:13 -07:00 |
Leni Aniva
|
6f85c262cf
|
feat: Instantiate mvars during echo
|
2024-03-31 17:09:24 -07:00 |
Leni Aniva
|
2130bcf357
|
test: Library test
|
2024-03-31 16:43:30 -07:00 |
Leni Aniva
|
52d3283b5c
|
refactor: Use library goalStartExpr function
|
2024-03-31 16:06:30 -07:00 |
Leni Aniva
|
65ac0d5c58
|
feat: Specify type in echo
|
2024-03-31 15:55:08 -07:00 |
Leni Aniva
|
90f7f251e9
|
Merge branch 'dev' into io/serial
|
2024-03-30 00:07:46 -07:00 |
Leni Aniva
|
113e65e193
|
Merge branch 'dev' into goal/relation
|
2024-03-29 23:47:09 -07:00 |
Leni Aniva
|
bc83a5732e
|
feat: Instantiation tests
Note that delay assigned metavariables are not instantiated.
|
2024-03-29 23:46:08 -07:00 |
Leni Aniva
|
78a3b240ba
|
test: Catalog has no numeric symbols
|
2024-03-28 20:44:09 -07:00 |
Leni Aniva
|
35c4ea693d
|
feat: Stop cataloging internal/detail dependencies
|
2024-03-28 19:49:44 -07:00 |
Leni Aniva
|
d9af064888
|
test: Elimination of aux lemmas
|
2024-03-28 19:27:45 -07:00 |
Leni Aniva
|
01a23b338a
|
feat: Unfold aux lemmas when printing root expr
|
2024-03-28 18:56:42 -07:00 |
Leni Aniva
|
60903bf31f
|
feat: Bump toolchain version
|
2024-03-28 00:06:35 -07:00 |
Leni Aniva
|
689112d973
|
fix: Use Arrays only in the ABI
|
2024-03-14 22:40:14 -07:00 |
Leni Aniva
|
8853b17fee
|
test: More diagnostics for tests
|
2024-03-06 15:14:08 -08:00 |
Leni Aniva
|
d57612ec71
|
test: Delayed metavariable assignment
|
2024-02-15 14:47:09 -08:00 |
Leni Aniva
|
5720c72515
|
feat: Prevent crash during rootExpr call
|
2024-01-30 17:22:20 -08:00 |
Leni Aniva
|
9a5ee49778
|
feat: Print parent expression assignment
|
2024-01-24 18:19:04 -08:00 |
Leni Aniva
|
93a34f9fda
|
feat: Print constructor and recursor info
|
2024-01-16 14:11:52 -08:00 |
Leni Aniva
|
a1421439f8
|
feat: Print inductives in env.inspect
|
2024-01-16 13:29:30 -08:00 |
Leni Aniva
|
b29f7cb180
|
test: Simplify monad execution
|
2024-01-07 14:14:20 -08:00 |
Leni Aniva
|
77232d5a1e
|
refactor: Rename Test/{Catalog,Environment}
|
2023-12-26 12:22:57 -05:00 |
Leni Aniva
|
22789436bd
|
chore: Move environment functions to its own file
Symbol.lean is now subsumed
|
2023-12-15 13:40:36 -05:00 |
Leni Aniva
|
3b83c81540
|
fix: Force instantiate all mvars in env.add
|
2023-12-15 13:07:59 -05:00 |
Leni Aniva
|
6c25cca46a
|
test: env.add
|
2023-12-14 11:11:24 -08:00 |
Leni Aniva
|
09f5792d4a
|
Merge branch 'dev' into env/add-decl
|
2023-12-14 05:48:49 -08:00 |
Leni Aniva
|
12544b81ee
|
chore: Rename lib. commands to env.
This is done to improve clarity and align with Lean's terminology
|
2023-12-12 18:56:25 -08:00 |
Leni Aniva
|
ab1b309c72
|
feat: Use CoreM as the main interaction monad
|
2023-12-12 18:39:02 -08:00 |
Leni Aniva
|
c76751861a
|
fix: Change the main interaction monad to MetaM
|
2023-12-08 16:17:16 -08:00 |
Leni Aniva
|
9276d47e0d
|
Merge branch 'dev' into library/catalog
|
2023-12-05 20:21:22 -08:00 |
Leni Aniva
|
da74258dd1
|
feat!: Display public name only if name is private
|
2023-12-05 20:20:08 -08:00 |
Leni Aniva
|
9f2b07757f
|
feat: Display whether a symbol is private
|
2023-12-05 19:07:00 -08:00 |
Leni Aniva
|
ec09304e02
|
feat: Remove printing projections
|
2023-12-04 16:21:02 -08:00 |
Leni Aniva
|
736e68639f
|
fix: New goal state not inserted correctly
|
2023-11-07 13:07:50 -08:00 |
Leni Aniva
|
245e76b2f1
|
feat: Print the root mvar name
|
2023-11-06 11:51:31 -08:00 |
Leni Aniva
|
7c28cf4ed0
|
Merge branch 'dev' into goal/continuation
|
2023-11-06 11:45:24 -08:00 |
Leni Aniva
|
c5f563598d
|
chore: Remove unnecessary unsafe's
|
2023-11-06 11:43:57 -08:00 |
Leni Aniva
|
dbace9f2d5
|
fix: Use Lean's built in name parser
The `str_to_name` parser cannot handle numerical names and escapes.
|
2023-11-06 10:45:11 -08:00 |
Leni Aniva
|
d809a960f9
|
feat: Goal continuation fails if target has goals
|
2023-11-04 15:53:57 -07:00 |
Leni Aniva
|
754fb69cff
|
feat: Partial state continuation
|
2023-11-04 15:33:53 -07:00 |
Leni Aniva
|
dc2cc5be77
|
test: Separate mvar coupling tests
|
2023-11-04 15:01:41 -07:00 |
Leni Aniva
|
8dd994d1ca
|
bug: Fix quote escape problem
|
2023-10-30 14:45:43 -07:00 |
Leni Aniva
|
d87217c6bb
|
feat: Print metavariable name in goal
|
2023-10-30 14:44:06 -07:00 |
Leni Aniva
|
454a5bc6b9
|
feat: Simplify printing of function applications
|
2023-10-29 12:50:36 -07:00 |
Leni Aniva
|
e2526f11b1
|
feat: Print names in one segment separated with .
|
2023-10-29 11:56:56 -07:00 |
Leni Aniva
|
c2d606b9d9
|
feat: Simplify name printing
|
2023-10-29 11:18:35 -07:00 |
Leni Aniva
|
427d819349
|
feat: Add REPL function for root expression
|
2023-10-27 15:41:12 -07:00 |