Leni Aniva
|
075bec6da2
|
feat: Output shared library in flake
|
2024-03-06 15:26:35 -08:00 |
Leni Aniva
|
3292b34070
|
Merge pull request 'feat: Print parent expression assignment' (#45) from goal/relation into dev
Reviewed-on: #45
|
2024-02-15 14:55:02 -08:00 |
Leni Aniva
|
d57612ec71
|
test: Delayed metavariable assignment
|
2024-02-15 14:47:09 -08:00 |
Leni Aniva
|
9ac84b3fd1
|
Merge branch 'dev' into goal/relation
|
2024-02-15 14:39:30 -08:00 |
Leni Aniva
|
a748900ad6
|
Merge pull request 'feat: Add leanpkgs to the flake output' (#46) from nix/toolchain into dev
Reviewed-on: #46
|
2024-02-15 14:30:30 -08:00 |
Leni Aniva
|
3e321516f7
|
chore: Expose `leanPkgs` in flake
|
2024-02-13 15:30:56 -05:00 |
Leni Aniva
|
8b67e7006a
|
feat: Add lake and lean to the package output
|
2024-02-05 11:50:22 -08:00 |
Leni Aniva
|
4a98b90289
|
chore: Version bump to 0.2.12-alpha
|
2024-01-30 17:45:32 -08:00 |
Leni Aniva
|
5720c72515
|
feat: Prevent crash during rootExpr call
|
2024-01-30 17:22:20 -08:00 |
Leni Aniva
|
6d22841a27
|
doc: Correct comment about parent filling expr
|
2024-01-30 16:37:35 -08:00 |
Leni Aniva
|
9a5ee49778
|
feat: Print parent expression assignment
|
2024-01-24 18:19:04 -08:00 |
Leni Aniva
|
a811decf84
|
Merge pull request 'test: Option controlled mvar instantiation' (#44) from goal/diag into dev
Reviewed-on: #44
|
2024-01-17 22:27:44 -08:00 |
Leni Aniva
|
79b6974172
|
Merge branch 'dev' into goal/diag
|
2024-01-17 14:03:19 -08:00 |
Leni Aniva
|
42c3da4a67
|
Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43) from env/inspect into dev
Reviewed-on: #43
|
2024-01-17 14:02:55 -08:00 |
Leni Aniva
|
efa956464d
|
test: Option controlled mvar instantiation
|
2024-01-16 16:44:54 -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
|
6e39b5ef8b
|
Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev
Reviewed-on: #41
|
2023-12-26 12:41:01 -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
|
aca7dc9811
|
refactor: env. operations into its own file
|
2023-12-15 13:37:55 -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
|
2f3a91562a
|
fix: env_add monads
|
2023-12-14 05:52:12 -08:00 |
Leni Aniva
|
09f5792d4a
|
Merge branch 'dev' into env/add-decl
|
2023-12-14 05:48:49 -08:00 |
Leni Aniva
|
4076d8a7dd
|
Merge pull request 'feat: Change the main interaction monad' (#40) from core/loop into dev
Reviewed-on: #40
|
2023-12-14 05:46:39 -08:00 |
Leni Aniva
|
02889510b2
|
feat: env_add command
|
2023-12-13 19:35:32 -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
|
45beca0bc4
|
doc: TermElabM metavariable generation
|
2023-12-08 17:32:30 -08:00 |
Leni Aniva
|
1fb189a38f
|
fix: Consolidate TermElabM blocks
|
2023-12-08 17:31:25 -08:00 |
Leni Aniva
|
c76751861a
|
fix: Change the main interaction monad to MetaM
|
2023-12-08 16:17:16 -08:00 |
Leni Aniva
|
de2688ccfa
|
chore: Version downgrade to 0.2.10-alpha
There is a currently known bug
|
2023-12-07 12:38:02 -08:00 |
Leni Aniva
|
4871133027
|
Merge pull request 'fix: Printing projection leads to crash' (#37) from io/sexp into dev
Reviewed-on: #37
|
2023-12-07 12:33:01 -08:00 |
Leni Aniva
|
2dc7657e2a
|
doc: getUsedConstants bug about projections
|
2023-12-06 15:05:04 -08:00 |
Leni Aniva
|
ccf5a03647
|
fix: Printing projection leads to crash
|
2023-12-05 22:45:59 -08:00 |
Leni Aniva
|
56966b27cf
|
Merge pull request 'feat: Handling of private names' (#36) from library/catalog into dev
Reviewed-on: #36
|
2023-12-05 20:22:38 -08:00 |
Leni Aniva
|
9276d47e0d
|
Merge branch 'dev' into library/catalog
|
2023-12-05 20:21:22 -08:00 |
Leni Aniva
|
cf856d2880
|
chore: Version bump
|
2023-12-05 20:21:07 -08:00 |
Leni Aniva
|
beb837ccab
|
Merge pull request 'feat: Print structural projection as application' (#35) from io/serial into dev
Reviewed-on: #35
|
2023-12-05 20:20:51 -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
|
07ade4c822
|
feat: Expose _private names
|
2023-12-04 23:36:09 -08:00 |
Leni Aniva
|
a454aaf1d4
|
feat: Remove stem deduce
Some private subproofs are not shown in the catalog and this breaks
dependencies
|
2023-12-04 16:40:15 -08:00 |
Leni Aniva
|
ec09304e02
|
feat: Remove printing projections
|
2023-12-04 16:21:02 -08:00 |
Leni Aniva
|
967e3dfb4f
|
feat: Remove | in symbol output
|
2023-11-27 09:54:41 -08:00 |
Leni Aniva
|
0a5a96275f
|
chore: Version bump to 0.2.9
|
2023-11-26 23:48:47 -08:00 |
Leni Aniva
|
7690272bfa
|
feat: Shorter symbol category
|
2023-11-26 22:14:58 -08:00 |
Leni Aniva
|
7b59937853
|
feat: Read dependencies of library symbols
|
2023-11-25 15:07:56 -08:00 |