 Leni Aniva
|
50ac2fea4b
|
feat: Print constructor and recursor info
|
2024-01-16 14:11:52 -08:00 |
|
Leni Aniva
|
6fb1b2e787
|
feat: Print inductives in env.inspect
|
2024-01-16 13:29:30 -08:00 |
|
Leni Aniva
|
6692303da6
|
test: Simplify monad execution
|
2024-01-07 14:14:20 -08:00 |
|
Leni Aniva
|
a8bfa56587
|
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
|
1c370ef2ae
|
refactor: Rename Test/{Catalog,Environment}
|
2023-12-26 12:22:57 -05:00 |
|
Leni Aniva
|
dc90b6b73e
|
chore: Move environment functions to its own file
Symbol.lean is now subsumed
|
2023-12-15 13:40:36 -05:00 |
|
Leni Aniva
|
da194a1165
|
refactor: env. operations into its own file
|
2023-12-15 13:37:55 -05:00 |
|
Leni Aniva
|
aef93cf506
|
fix: Force instantiate all mvars in env.add
|
2023-12-15 13:07:59 -05:00 |
|
Leni Aniva
|
a540dd4540
|
test: env.add
|
2023-12-14 11:11:24 -08:00 |
|
Leni Aniva
|
85eb42207c
|
fix: env_add monads
|
2023-12-14 05:52:12 -08:00 |
|
Leni Aniva
|
69be7c3920
|
Merge branch 'dev' into env/add-decl
|
2023-12-14 05:48:49 -08:00 |
|
Leni Aniva
|
83ff58dffc
|
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
|
3c96a7c0ea
|
feat: env_add command
|
2023-12-13 19:35:32 -08:00 |
|
Leni Aniva
|
ff4671cdd0
|
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
|
085b12c255
|
feat: Use CoreM as the main interaction monad
|
2023-12-12 18:39:02 -08:00 |
|
Leni Aniva
|
ac9f6f810c
|
doc: TermElabM metavariable generation
|
2023-12-08 17:32:30 -08:00 |
|
Leni Aniva
|
bd0c66facc
|
fix: Consolidate TermElabM blocks
|
2023-12-08 17:31:25 -08:00 |
|
Leni Aniva
|
2fe4fa9bc4
|
fix: Change the main interaction monad to MetaM
|
2023-12-08 16:17:16 -08:00 |
|
Leni Aniva
|
d7fcc502f9
|
chore: Version downgrade to 0.2.10-alpha
There is a currently known bug
|
2023-12-07 12:38:02 -08:00 |
|
Leni Aniva
|
94c4b2cfe3
|
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
|
924a67f46d
|
doc: getUsedConstants bug about projections
|
2023-12-06 15:05:04 -08:00 |
|
Leni Aniva
|
8a8db545a5
|
fix: Printing projection leads to crash
|
2023-12-05 22:45:59 -08:00 |
|
Leni Aniva
|
f2b54ec018
|
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
|
3c2d93259f
|
Merge branch 'dev' into library/catalog
|
2023-12-05 20:21:22 -08:00 |
|
Leni Aniva
|
079f12d6d3
|
chore: Version bump
|
2023-12-05 20:21:07 -08:00 |
|
Leni Aniva
|
d846210b9e
|
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
|
dbfee00420
|
feat!: Display public name only if name is private
|
2023-12-05 20:20:08 -08:00 |
|
Leni Aniva
|
cdb1e8576f
|
feat: Display whether a symbol is private
|
2023-12-05 19:07:00 -08:00 |
|
Leni Aniva
|
c80d7567b6
|
feat: Expose _private names
|
2023-12-04 23:36:09 -08:00 |
|
Leni Aniva
|
f72a82a4c9
|
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
|
35f411041e
|
feat: Remove printing projections
|
2023-12-04 16:21:02 -08:00 |
|
Leni Aniva
|
860d2e239a
|
feat: Remove | in symbol output
|
2023-11-27 09:54:41 -08:00 |
|
Leni Aniva
|
e0cfdfaf16
|
chore: Version bump to 0.2.9
|
2023-11-26 23:48:47 -08:00 |
|
Leni Aniva
|
fe850ded98
|
feat: Shorter symbol category
|
2023-11-26 22:14:58 -08:00 |
|
Leni Aniva
|
aaebb6b121
|
feat: Read dependencies of library symbols
|
2023-11-25 15:07:56 -08:00 |
|
Leni Aniva
|
a1d991f5db
|
fix: Rectify error format
|
2023-11-09 22:24:17 -08:00 |
|
Leni Aniva
|
cc9e659c06
|
Merge pull request 'feat: Allow selective continuation of goals' (#27) from goal/continuation into dev
Reviewed-on: #27
|
2023-11-07 16:49:55 -08:00 |
|
Leni Aniva
|
a491316541
|
fix: Do not show parent state in continue
|
2023-11-07 13:10:14 -08:00 |
|
Leni Aniva
|
e654613182
|
fix: New goal state not inserted correctly
|
2023-11-07 13:07:50 -08:00 |
|
Leni Aniva
|
d35803791e
|
Merge branch 'dev' into goal/continuation
|
2023-11-07 12:11:14 -08:00 |
|
Leni Aniva
|
d9745094fa
|
fix: Remove the error prone SemihashMap
|
2023-11-07 12:09:54 -08:00 |
|
Leni Aniva
|
53b63bf46c
|
fix: Remove the error prone SemihashMap
|
2023-11-07 12:04:17 -08:00 |
|
Leni Aniva
|
4396da3e65
|
chore: Code formatting
|
2023-11-06 12:20:08 -08:00 |
|
Leni Aniva
|
ce585f7288
|
feat: Print the root mvar name
|
2023-11-06 11:51:31 -08:00 |
|
Leni Aniva
|
32fedede6a
|
Merge branch 'dev' into goal/continuation
|
2023-11-06 11:45:24 -08:00 |
|
Leni Aniva
|
8182da436d
|
chore: Remove unnecessary unsafe's
|
2023-11-06 11:43:57 -08:00 |
|
Leni Aniva
|
c6bb4be597
|
chore: Update documentation
|
2023-11-06 11:04:28 -08:00 |
|
Leni Aniva
|
ce1cb13e54
|
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
|
a5b5e01858
|
chore: Version bump to 0.2.8
|
2023-11-04 15:54:28 -07:00 |
|
Leni Aniva
|
4be9dbc84a
|
feat: Goal continuation fails if target has goals
|
2023-11-04 15:53:57 -07:00 |