Leni Aniva
773a0afbd8
feat: Handling of universe level names in elab
2024-06-11 12:44:42 -07:00
Leni Aniva
bbc00cbbb8
feat: Congruence tactic FFI interface and tests
2024-05-20 14:00:04 -07:00
Leni Aniva
75df7268c5
test: Simplify testing structure for tactics
2024-05-20 11:55:38 -07:00
Leni Aniva
92acf7782c
test: CongruenceArg tactic
2024-05-20 11:51:35 -07:00
Leni Aniva
2f951c8fef
fix: Decoupling of mvars during instantiation
2024-05-19 15:43:10 -07:00
Leni Aniva
6ad24b72d4
fix: Nested delayed assignment instantiation
2024-05-16 10:31:38 -07:00
Leni Aniva
cf17428001
fix: Panic in partial instantiation
2024-05-15 21:34:36 -07:00
Leni Aniva
5c7bb288b2
feat: Display full free variable list in subst
2024-05-14 19:09:04 -07:00
Leni Aniva
f813d4a8dd
refactor: Delayed mvar instantiation function
2024-05-13 13:49:05 -07:00
Leni Aniva
c04b363de7
feat: Handle delay assigned mvars
2024-05-12 22:33:38 -07:00
Leni Aniva
03ecb6cf19
feat: Partial instantiate metavariables
2024-05-11 20:01:34 -07:00
Leni Aniva
0b88f6708e
test: Delayed mvar assignment for mapply
2024-05-09 14:02:43 -07:00
Leni Aniva
69ec70ffbe
feat: Do not explicitly show delay assigned mvar
2024-05-06 22:39:17 -07:00
Leni Aniva
cf1289f159
feat: NoConfuse tactic
2024-05-05 13:24:29 -07:00
Leni Aniva
1e1995255a
test: mapply captures dependent types
2024-05-05 10:36:43 -07:00
Leni Aniva
4cff6677d2
chore: Lean version bump to 4.8.0-rc1
2024-05-04 23:36:42 -07:00
Leni Aniva
6ffb227cd6
feat: Conduit modus ponens
2024-04-22 10:02:09 -07:00
Leni Aniva
feff62a3c5
fix: Remove determination of major
2024-04-22 09:52:13 -07:00
Leni Aniva
3812aa56ec
feat: Phantom var in mapply
2024-04-22 00:11:41 -07:00
Leni Aniva
4a92e655f6
test: Tactic test stub
2024-04-20 13:09:41 -07:00
Leni Aniva
fec13ddb51
chore: Code cleanup
2024-04-18 14:19:25 -07:00
Leni Aniva
dbd54f7679
feat: Implement the mapply tactic
2024-04-15 12:47:02 -07:00
Leni Aniva
614b9aa4ae
Merge branch 'dev' into goal/let
2024-04-12 21:41:56 -07:00
Leni Aniva
b45b90b810
test: Metavariable name matches in let
2024-04-12 21:41:16 -07:00
Leni Aniva
77907fd060
feat: `goalLet` function
2024-04-12 21:30:56 -07:00
Leni Aniva
4ee955c21f
test: Tests the `let` tactic
2024-04-12 21:16:00 -07:00
Leni Aniva
4b01af7cef
Merge branch 'dev' into serial/goal
2024-04-12 20:52:38 -07:00
Leni Aniva
e5d55e31ff
feat: Print expression dependent mvars
2024-04-12 20:51:54 -07:00
Leni Aniva
8e377c2092
refactor: CamelCase rename
2024-04-12 16:34:21 -07:00
Leni Aniva
991ee5ad94
refactor: Rename functions to camel case
2024-04-12 12:37:37 -07:00
Leni Aniva
036fab0ad6
fix: Prevent incorrect inheritance of calc rhs
2024-04-11 16:15:58 -07:00
Leni Aniva
a41b95e540
Merge branch 'dev' into goal/have-conv-calc
2024-04-11 15:35:30 -07:00
Leni Aniva
a11df9f2e9
feat: Print recursor rules
2024-04-11 15:35:14 -07:00
Leni Aniva
535770bbd7
feat: Calc tactic
2024-04-11 14:59:55 -07:00
Leni Aniva
823c9635c7
fix: Leading element in .proj sexp
2024-04-09 10:06:26 -07:00
Leni Aniva
55b44c3fa1
fix: Serialization of .proj
2024-04-09 10:03:36 -07:00
Leni Aniva
22bb818a1c
refactor: Use the `tactic interface for `conv
2024-04-08 12:32:27 -07:00
Leni Aniva
63e64a1e9f
feat: Conv tactic functions
2024-04-08 12:26:22 -07:00
Leni Aniva
19d2f5ff3f
feat: Conv tactic mode
2024-04-07 17:03:49 -07:00
Leni Aniva
d9ed051b4d
feat: Partial implementation of `conv`
2024-04-07 14:22:20 -07:00
Leni Aniva
38cb91652f
Merge branch 'dev' into goal/have-conv-calc
2024-04-06 22:04:52 -07:00
Leni Aniva
7fe73551c3
feat: The `have` tactic
2024-04-06 21:52:25 -07:00
Leni Aniva
5a60ca74d5
fix: Auto bound implicit in elab
2024-04-06 17:45:36 -07:00
Leni Aniva
41cb3f68cd
test: Tests for conv and calc
2024-04-06 17:22:09 -07:00
Leni Aniva
1b7b6a644b
feat: `GoalState.tryHave` tactic (tests failing)
2024-04-06 16:33:20 -07:00
Leni Aniva
92351c9a3d
test: Move parallelism to Test/Main.lean
2024-04-06 14:14:30 -07:00
Leni Aniva
8a447e67cd
test: Parallel testing infrastructure
2024-04-06 14:07:13 -07:00
Leni Aniva
8b43dc0f25
feat: Instantiate mvars during echo
2024-03-31 17:09:24 -07:00
Leni Aniva
216bb9e920
test: Library test
2024-03-31 16:43:30 -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
2c48ff9e42
Merge branch 'dev' into io/serial
2024-03-30 00:07:46 -07:00
Leni Aniva
10e6877f0e
Merge branch 'dev' into goal/relation
2024-03-29 23:47:09 -07:00
Leni Aniva
252f85e66c
feat: Instantiation tests
...
Note that delay assigned metavariables are not instantiated.
2024-03-29 23:46:08 -07:00
Leni Aniva
e79e386b39
test: Catalog has no numeric symbols
2024-03-28 20:44:09 -07:00
Leni Aniva
8fa1a7d383
feat: Stop cataloging internal/detail dependencies
2024-03-28 19:49:44 -07:00
Leni Aniva
9e68a9cae4
test: Elimination of aux lemmas
2024-03-28 19:27:45 -07:00
Leni Aniva
a698a4250f
feat: Unfold aux lemmas when printing root expr
2024-03-28 18:56:42 -07:00
Leni Aniva
516ab15961
feat: Bump toolchain version
2024-03-28 00:06:35 -07:00
Leni Aniva
e6dbf88ce2
fix: Use Arrays only in the ABI
2024-03-14 22:40:14 -07:00
Leni Aniva
7e28ded23f
test: More diagnostics for tests
2024-03-06 15:14:08 -08:00
Leni Aniva
111781816f
test: Delayed metavariable assignment
2024-02-15 14:47:09 -08:00
Leni Aniva
fe5c1eda7d
feat: Prevent crash during rootExpr call
2024-01-30 17:22:20 -08:00
Leni Aniva
25f3a2f19d
feat: Print parent expression assignment
2024-01-24 18:19:04 -08:00
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
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
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
69be7c3920
Merge branch 'dev' into env/add-decl
2023-12-14 05:48:49 -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
2fe4fa9bc4
fix: Change the main interaction monad to MetaM
2023-12-08 16:17:16 -08:00
Leni Aniva
3c2d93259f
Merge branch 'dev' into library/catalog
2023-12-05 20:21:22 -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
35f411041e
feat: Remove printing projections
2023-12-04 16:21:02 -08:00
Leni Aniva
e654613182
fix: New goal state not inserted correctly
2023-11-07 13:07:50 -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
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
4be9dbc84a
feat: Goal continuation fails if target has goals
2023-11-04 15:53:57 -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
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
60854525b9
feat: Simplify printing of function applications
2023-10-29 12:50:36 -07:00
Leni Aniva
de250eafd0
feat: Print names in one segment separated with .
2023-10-29 11:56:56 -07:00
Leni Aniva
c0dfa04b18
feat: Simplify name printing
2023-10-29 11:18:35 -07:00
Leni Aniva
045181356c
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
3b1746490d
feat: Add REPL command for assigning an expression
2023-10-27 15:32:59 -07:00
Leni Aniva
f064bb21a4
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
269e5c707c
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
c852db2f46
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
8029298db7
feat: Display user name in Goal structure
...
1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression
2023-10-25 22:18:59 -07:00
Leni Aniva
d991533170
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07:00
Leni Aniva
538ba6e7d7
Store states instead of goals
...
1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)
Documentations pending
2023-10-15 17:15:23 -07:00
Leni Aniva