 Leni Aniva
|
7acf1ffdf1
|
refactor: Move `have` to prograde tactic
|
2024-06-25 16:58:35 -04:00 |
|
Leni Aniva
|
2d2cf75183
|
Merge branch 'dev' into goal/mapply
|
2024-06-12 13:44:49 -07:00 |
|
Leni Aniva
|
c0e6e3ec39
|
Merge branch 'parse/level' into goal/mapply
|
2024-06-11 15:21:35 -07:00 |
|
Leni Aniva
|
773a0afbd8
|
feat: Handling of universe level names in elab
|
2024-06-11 12:44:42 -07:00 |
|
Leni Aniva
|
855e771609
|
feat: Add compilation unit boundary command
|
2024-05-31 16:35:46 -07:00 |
|
Leni Aniva
|
09628309a9
|
feat: Basic tactic extraction (before/after/tactic)
|
2024-05-28 17:25:22 -07:00 |
|
Leni Aniva
|
cf1c884c8c
|
Merge branch 'dev' into goal/mapply
|
2024-05-20 11:08:14 -07:00 |
|
Leni Aniva
|
4cff6677d2
|
chore: Lean version bump to 4.8.0-rc1
|
2024-05-04 23:36:42 -07:00 |
|
Leni Aniva
|
adbb07af2d
|
fix: Option setting in REPL
|
2024-04-12 22:39:47 -07:00 |
|
Leni Aniva
|
dc6e79def7
|
doc: Update error message in interaction
|
2024-04-11 16:18:04 -07:00 |
|
Leni Aniva
|
7eb5419f36
|
feat: REPL interface for `calc`
|
2024-04-11 15:11:10 -07:00 |
|
Leni Aniva
|
63e64a1e9f
|
feat: Conv tactic functions
|
2024-04-08 12:26:22 -07:00 |
|
Leni Aniva
|
058f5a98b2
|
feat: Bindings for the `have` tactic
|
2024-04-06 16:40:22 -07:00 |
|
Leni Aniva
|
216bb9e920
|
test: Library test
|
2024-03-31 16:43:30 -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
|
3debcc021a
|
feat(lib): Export goal.print function
|
2024-03-14 16:34:01 -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
|
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 |
|
Leni Aniva
|
25f3a2f19d
|
feat: Print parent expression assignment
|
2024-01-24 18:19:04 -08: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
|
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
|
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
|
924a67f46d
|
doc: getUsedConstants bug about projections
|
2023-12-06 15:05:04 -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
|
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
|
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
|
d9745094fa
|
fix: Remove the error prone SemihashMap
|
2023-11-07 12:09:54 -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
|
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
|
97d658cfc5
|
feat: Add goal.continue command
|
2023-11-04 15:51:09 -07:00 |
|
Leni Aniva
|
045181356c
|
feat: Add REPL function for root expression
|
2023-10-27 15:41:12 -07:00 |