288 Commits

Author	SHA1	Message	Date
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