Commit Graph

176 Commits

Author SHA1 Message Date
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
Leni Aniva 97d658cfc5 feat: Add goal.continue command 2023-11-04 15:51:09 -07:00
Leni Aniva 333355a85d feat: Partial state continuation 2023-11-04 15:33:53 -07:00
Leni Aniva 4a4a33cea7 test: Separate mvar coupling tests 2023-11-04 15:01:41 -07:00
Leni Aniva 1638c308a9 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev
Reviewed-on: #26
2023-10-30 14:47:41 -07:00
Leni Aniva 59ac83f0b7 bug: Fix quote escape problem 2023-10-30 14:45:43 -07:00
Leni Aniva d1c0dc376f feat: Print metavariable name in goal 2023-10-30 14:44:06 -07:00
Leni Aniva 6cf328a84f Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
Reviewed-on: #25
2023-10-29 13:08:05 -07:00