Leni Aniva
3733c10a4e
refactor: Unify call convention
...
Induction like tactics should return `Array InductionSubgoal`. Branching
tactics should return their branch first.
2024-08-17 16:47:21 -07:00
Leni Aniva
43e11f1ba3
refactor: Always display isInaccessible
2024-08-17 00:53:38 -07:00
Leni Aniva
0c469027c6
fix: Refactor mvar collection in assign tactic
2024-08-17 00:50:02 -07:00
Leni Aniva
e1b7eaab12
fix: Let tactic not bringing binder into scope
2024-08-17 00:47:12 -07:00
Leni Aniva
d17b21e282
fix: Use `getMVarsNoDelayed`
2024-08-16 00:32:34 -07:00
Leni Aniva
5b4f8a37eb
refactor: All Tactic/ tactics into MetaM form
2024-08-15 23:41:17 -07:00
Leni Aniva
1e7a186bb1
refactor: MetaM form of define (evaluate)
2024-08-15 23:23:17 -07:00
Leni Aniva
9b0456a5e0
refactor: MetaM form of have and let
2024-08-15 23:17:15 -07:00
Leni Aniva
7968072097
refactor: Remove the newMVarSet mechanism
...
This field has ambiguous purpose and does not account for different
types of mvars
2024-08-15 22:53:42 -07:00
Leni Aniva
e07f9d9b3f
Merge branch 'dev' into tactic/eval
2024-08-15 22:45:43 -07:00
Leni Aniva
e943a4b065
refactor: Assign into its own tactic
2024-08-15 22:39:40 -07:00
Leni Aniva
0bc7bc5856
refactor: Remove export of Lean functions
...
If the user wishes to use Lean functions, they should add the bindings manually.
2024-08-14 01:20:56 -07:00
Leni Aniva
c9ee31bbfd
feat: Export `mkFun`
2024-08-02 22:33:03 -07:00
Leni Aniva
394fb73137
feat: Add direct expression to string
2024-08-02 22:00:27 -07:00
Leni Aniva
c0e2a592ea
feat: Expose `mkAppM'`
2024-08-02 21:44:46 -07:00
Leni Aniva
2c08ef1e23
refactor: Remove old `visibleFVars` interface
2024-08-02 19:53:19 -07:00
Leni Aniva
651afa75f4
feat: Filter in `visibleFVarsOfMVar`
2024-08-02 19:49:11 -07:00
Leni Aniva
abef7a6f0d
feat: Export fvar names function
2024-07-31 00:00:33 -07:00
Leni Aniva
caa463f410
feat: Export GoalState.goalsArray
2024-07-30 17:02:41 -07:00
Leni Aniva
3ca52517ab
feat: Refactor out projToApp
2024-07-30 13:30:41 -07:00
Leni Aniva
1c9a411d4d
feat: Export constant info type/value
2024-07-29 18:39:22 -07:00
Leni Aniva
7b5567d784
fix: Name internal order
2024-07-28 14:19:47 -07:00
Leni Aniva
29f437f859
feat: Export GoalState.create
2024-07-28 13:58:20 -07:00
Leni Aniva
4c81f226d1
feat: Expose environment functions
2024-07-28 13:46:14 -07:00
Leni Aniva
9db5463499
feat: Export `GoalState.resume`
2024-07-27 18:20:34 -07:00
Leni Aniva
bf941cd686
feat: Expose parent and root expr functions
2024-07-27 17:39:51 -07:00
Leni Aniva
2682ce5b7b
refactor: Move condensed functions to condensed
2024-07-23 11:57:12 -07:00
Leni Aniva
3b415e8dc1
chore: Rename exports
2024-07-23 05:16:46 -07:00
Leni Aniva
431ca4e481
fix: Move elab context to condensed
2024-07-22 17:57:01 -07:00
Leni Aniva
eb5ee8c57c
feat: Expose TermElab context and state
2024-07-22 17:34:14 -07:00
Leni Aniva
94c7b021f7
fix: Signature of ppExpr
2024-07-15 12:22:47 -07:00
Leni Aniva
193d94e798
feat: Expression creation and pretty printing
2024-07-15 11:42:02 -07:00
Leni Aniva
a7fe7cbd7c
Merge branch 'misc/version' into serial/expr
2024-07-15 09:53:36 -07:00
Leni Aniva
4549ae1f65
Merge branch 'misc/version' into tactic/eval
2024-07-06 19:56:31 -07:00
Leni Aniva
c404564a2b
chore: Bump Lean version to 4.10.0-rc1
2024-07-06 19:53:50 -07:00
Leni Aniva
6ddde2963d
test: Eval instantiate
2024-06-27 14:51:16 -04:00
Leni Aniva
2d2ff24017
feat: FFI interface for `evaluate` tactic
2024-06-25 17:10:31 -04:00
Leni Aniva
7acf1ffdf1
refactor: Move `have` to prograde tactic
2024-06-25 16:58:35 -04:00
Leni Aniva
c0124b347f
Merge branch 'serial/expr' into tactic/eval
2024-06-25 16:05:20 -04:00
Leni Aniva
8e78718447
feat: Extract MetaM context and state from goal
2024-06-25 15:54:55 -04:00
Leni Aniva
ffbea41f62
feat: Condensed interface
2024-06-25 15:13:58 -04:00
Leni Aniva
e282d9f781
test: Evaluation tactic
2024-06-25 11:03:08 -04:00
Leni Aniva
25a7025c25
feat: Evaluation tactic
2024-06-23 15:01:51 -07:00
Leni Aniva
aceee85b05
Merge branch 'env/inspect' into tactic/congruence
2024-06-16 13:46:18 -07:00
Leni Aniva
8707dbc9bb
fix: aux lemmas in env inspect
2024-06-16 13:44:57 -07:00
Leni Aniva
f80d90ce87
fix: Goal diag missing newline character
2024-06-14 11:59:02 -07:00
Leni Aniva
b3a60fcea8
refactor: Rename TacticExecute to SyntheticTactic
2024-06-13 14:25:05 -07: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
3a53493089
feat: Show delayed assignment in goal diag
2024-06-05 16:14:52 -07:00
Leni Aniva
6dcff8b151
fix: Print diag in mvar context
2024-06-05 15:56:20 -07:00
Leni Aniva
3c90c94645
fix: Execute instantiateAll in goal state diag
2024-06-05 13:45:13 -07:00
Leni Aniva
a2c5c7448c
chore: Code simplification, version bump
2024-05-31 20:23:10 -07:00
Leni Aniva
855e771609
feat: Add compilation unit boundary command
2024-05-31 16:35:46 -07:00
Leni Aniva
b9b16ba0e9
refactor: Code cleanup
2024-05-28 20:24:23 -07:00
Leni Aniva
09628309a9
feat: Basic tactic extraction (before/after/tactic)
2024-05-28 17:25:22 -07:00
Leni Aniva
bd42c396d7
chore: Code cleanup
2024-05-20 14:19:10 -07:00
Leni Aniva
bbc00cbbb8
feat: Congruence tactic FFI interface and tests
2024-05-20 14:00:04 -07:00
Leni Aniva
92acf7782c
test: CongruenceArg tactic
2024-05-20 11:51:35 -07:00
Leni Aniva
cf1c884c8c
Merge branch 'dev' into goal/mapply
2024-05-20 11:08:14 -07:00
Leni Aniva
cc74d41b15
feat: Congruence tactics
2024-05-20 10:55:52 -07:00
Leni Aniva
2f951c8fef
fix: Decoupling of mvars during instantiation
2024-05-19 15:43:10 -07:00
Leni Aniva
e165e41efa
chore: Version bump to v4.8.0-rc1
2024-05-17 20:31:45 -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
bc09f4a29d
refactor: Expr related functions to Expr.lean
2024-05-13 13:58:50 -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
e58dbc66a9
fix: Consistent naming in library functions
2024-05-08 20:51:36 -07:00
Leni Aniva
66a5dfcf3c
feat: Diagnostics command for FFI users
2024-05-08 12:41:21 -07:00
Leni Aniva
69ec70ffbe
feat: Do not explicitly show delay assigned mvar
2024-05-06 22:39:17 -07:00
Leni Aniva
aa106f7591
feat: Do not filter mvars from mapply
2024-05-06 22:20:20 -07:00
Leni Aniva
679871cbc6
fix: NoConfuse arg name
2024-05-05 13:26:46 -07:00
Leni Aniva
2937675044
feat: Library interface for calling no_confuse
2024-05-05 13:25:48 -07:00
Leni Aniva
cf1289f159
feat: NoConfuse tactic
2024-05-05 13:24:29 -07:00
Leni Aniva
63417ef179
fix: Motive extra arguments not instiantiated
2024-05-05 00:43:32 -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
398b1c39ed
refactor: Common tactic execute function
2024-04-19 12:37:17 -07:00
Leni Aniva
fec13ddb51
chore: Code cleanup
2024-04-18 14:19:25 -07:00
Leni Aniva
7aa7e6d7e9
feat: Library interface for mapply
2024-04-15 12:56:28 -07:00
Leni Aniva
dbd54f7679
feat: Implement the mapply tactic
2024-04-15 12:47:02 -07:00
Leni Aniva
75b4648ba9
feat: mapply stub
2024-04-14 15:40:57 -07:00
Leni Aniva
b954f12526
refactor: Move all tactic operations to the bottom
2024-04-13 19:41:49 -07:00
Leni Aniva
adbb07af2d
fix: Option setting in REPL
2024-04-12 22:39:47 -07:00
Leni Aniva
614b9aa4ae
Merge branch 'dev' into goal/let
2024-04-12 21:41:56 -07:00
Leni Aniva
77907fd060
feat: `goalLet` function
2024-04-12 21:30:56 -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
7a4d462a87
Merge branch 'dev' into goal/calc
2024-04-11 17:58:45 -07:00
Leni Aniva
4d4f660f3f
chore: Update version
2024-04-11 17:57:24 -07:00
Leni Aniva
a864c4d3ff
refactor: Code simplification
2024-04-11 16:29:47 -07:00
Leni Aniva
e834765896
refactor: Code simplification
2024-04-11 16:25:17 -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
7eb5419f36
feat: REPL interface for `calc`
2024-04-11 15:11:10 -07:00
Leni Aniva
6d85c19589
feat: Add library bindings for calc
2024-04-11 15:04:36 -07:00
Leni Aniva
6b44d9ef14
fix: Remove `calcPrevRhs?` in non-calc tactics
2024-04-11 15:03: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
30c1fd894f
fix: Coupling from unrelated goals
2024-04-09 09:11:15 -07:00
Leni Aniva
f02f9592d7
feat: Focus command
2024-04-08 13:12:51 -07:00
Leni Aniva
0e63583a1d
refactor: Monads in library
2024-04-08 12:54:02 -07:00
Leni Aniva
d4e49310f0
feat: FFI interface to conv functions
2024-04-08 12:50:41 -07:00
Leni Aniva
2f48cfbc19
doc: Remove outdated comments
2024-04-08 12:45:03 -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
7af24a4f0a
Merge branch 'dev' into goal/have-conv-calc
2024-04-08 10:38:18 -07:00
Leni Aniva
09189ce600
perf: Lazy run print monads
2024-04-08 10:32:13 -07:00
Leni Aniva
19d2f5ff3f
feat: Conv tactic mode
2024-04-07 17:03:49 -07:00
Leni Aniva
d50720f622
refactor: Metavariable set diff function
2024-04-07 14:32:25 -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
058f5a98b2
feat: Bindings for the `have` tactic
2024-04-06 16:40:22 -07:00
Leni Aniva
1b7b6a644b
feat: `GoalState.tryHave` tactic (tests failing)
2024-04-06 16:33:20 -07:00
Leni Aniva
8b43dc0f25
feat: Instantiate mvars during echo
2024-03-31 17:09:24 -07:00
Leni Aniva
744c9ee286
Merge pull request 'feat: Specify type in echo' ( #55 ) from expr/echo into dev
...
Reviewed-on: #55
2024-03-31 16:45:43 -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
e9c9548f17
fix: unfoldAuxLemma should be coreM
2024-03-31 15:40:14 -07:00
Leni Aniva
2b71203c1e
fix: Instantiation causes infinite loop
2024-03-30 00:17:16 -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
46faa5c089
chore: Version bump
2024-03-28 22:08:22 -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
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
f016d60d07
chore: Version bump to 0.2.13
2024-03-16 19:00:28 -07:00
Leni Aniva
e6dbf88ce2
fix: Use Arrays only in the ABI
2024-03-14 22:40:14 -07:00
Leni Aniva
3debcc021a
feat(lib): Export goal.print function
2024-03-14 16:34:01 -07:00
Leni Aniva
4eec930dd4
fix: Pass options by reference
2024-03-11 21:31:59 -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
eeb149a32c
feat(lib): Search path function
2024-03-09 19:36:25 -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
7e28ded23f
test: More diagnostics for tests
2024-03-06 15:14:08 -08:00
Leni Aniva
4acd367ca7
chore: Version bump to 0.2.12-alpha
2024-01-30 17:45:32 -08:00
Leni Aniva
fe5c1eda7d
feat: Prevent crash during rootExpr call
2024-01-30 17:22:20 -08:00
Leni Aniva
40d61fecc5
doc: Correct comment about parent filling expr
2024-01-30 16:37:35 -08:00
Leni Aniva
25f3a2f19d
feat: Print parent expression assignment
2024-01-24 18:19:04 -08:00
Leni Aniva
34d9b02797
Merge branch 'dev' into goal/diag
2024-01-17 14:03:19 -08:00
Leni Aniva
6a81d83c1f
test: Option controlled mvar instantiation
2024-01-16 16:44:54 -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
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
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
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
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
8a8db545a5
fix: Printing projection leads to crash
2023-12-05 22:45:59 -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
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
d9745094fa
fix: Remove the error prone SemihashMap
2023-11-07 12:09:54 -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
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
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
1a99a2e7b2
fix: Sanitize name in universe levels
2023-10-29 13:03:48 -07:00
Leni Aniva
60854525b9
feat: Simplify printing of function applications
2023-10-29 12:50:36 -07:00
Leni Aniva
e523e8bcc6
chore: Version bump (breaking change)
2023-10-29 11:57:24 -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
41db295ff5
Rename tactic to goal and restructure
2023-10-15 12:31:22 -07:00
Leni Aniva
35b391881e
Add ready message to indicate the main loop is up
2023-10-02 10:14:03 -07:00
Leni Aniva
f538f580bd
Merge branch 'dev' into tactic/book
2023-08-30 19:17:25 -07:00
Leni Aniva
f1f1c20ff9
Add SemihashMap interface, rename proof commands to goal commands, allow deletion
2023-08-30 19:16:33 -07:00
Leni Aniva
6b96f7893f
Separate max and imax in sort level
2023-08-27 22:50:18 -07:00
Leni Aniva
b98304f78a
Version bump to 0.2.4 due to breaking change
2023-08-27 19:59:31 -07:00
Leni Aniva
a6e337a89e
Rename proof commands to goal commands
2023-08-27 19:58:52 -07:00
Leni Aniva
a86af1bc57
Add SemihashMap structure for goal bookkeeping
2023-08-27 19:53:09 -07:00
Leni Aniva
9c4c43a9f1
Remove the obsolete name field from proof tree structure
2023-08-26 18:50:15 -07:00
Leni Aniva
59c046efc6
Add proper printing of sorts
2023-08-23 12:51:06 -07:00
Leni Aniva
96cbbf2551
Add compressed json print option; Rearrange commands into hierarchy
2023-08-16 19:25:32 -07:00
Leni Aniva
b2ba26528d
Add proof variable delta; Bump version to 0.2.1
2023-08-15 15:40:54 -07:00
Leni Aniva
7771408de1
Add expression sexp printing (2/2)
2023-08-14 21:43:40 -07:00
Leni Aniva
9eadd1d4d4
Add expression sexp printing (1/2, tests pending)
2023-08-14 17:07:53 -07:00
Leni Aniva
5cedb9d88c
version bump, restructure
2023-08-13 21:19:06 -07:00
Leni Aniva
622aa7f969
Add documentation; Remove mathlib dependency
2023-06-09 14:45:45 -07:00
Leni Aniva
4613777607
Add json goal printing
2023-05-27 23:10:39 -07:00
Leni Aniva
3e05722d1e
Add back the clear command to reset state
2023-05-26 16:55:33 -07:00
Leni Aniva
068a188fea
Add expr.type
2023-05-25 13:40:03 -07:00
Leni Aniva
e0c5f76451
Rename tactic failure mode to avoid confusion
...
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva
95ed7d115c
Add expression binding printing and import Lean
2023-05-24 00:54:48 -07:00
Leni Aniva
1fed222f56
Use TermElabM as the main monad stack instead of IO
2023-05-23 05:12:46 -07:00
Leni Aniva
94bc3355a2
Save core state in proofs
2023-05-22 22:48:48 -07:00
Leni Aniva
ba779766c0
Rename ids so they are consistent
2023-05-22 19:51:16 -07:00
Leni Aniva
0f8df08dd5
Add module name for symbol
2023-05-22 16:00:41 -07:00
Leni Aniva
116c7ff4c6
Add option id handling with ?
2023-05-22 14:56:43 -07:00
Leni Aniva
6a71dad389
Add option format for proof output and test cases
2023-05-22 14:49:56 -07:00
Leni Aniva
46ccad1669
Add default arguments for Json
2023-05-22 00:49:37 -07:00
Leni Aniva
083ec8beec
Add REPL tactics
2023-05-21 17:41:39 -07:00
Leni Aniva
15aab3d31f
Remove ExceptT from main monad
...
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva
2a4d348aab
Add expression IO stub for constant types
2023-05-20 14:04:09 -07:00
Leni Aniva
8127e9ba06
Add alternative command input format and IO stub
2023-05-20 13:03:12 -07:00
Leni Aniva
e246fd961f
Add tactic state manipulation
2023-05-17 21:58:03 -07:00
Leni Aniva
4d636ec12b
Add stack size troubleshooting
2023-05-14 15:22:41 -07:00
Leni Aniva
d3af535652
Add unsafe filtering in catalog
2023-05-12 16:12:21 -07:00
Leni Aniva
b5cb464694
Add README and catalog functions
2023-05-09 22:51:19 -07:00
Leni Aniva
f6a520c7a0
Separate commands into its own file
2023-05-09 18:01:09 -07:00
Leni Aniva