290 Commits

Author	SHA1	Message	Date
Leni Aniva	4bfd606e2a	Merge branch 'dev' into serial/pickle	2024-11-15 23:09:08 -08:00
Leni Aniva	2790553180	feat: Environment save/load commands	2024-11-13 19:50:31 -08:00
Leni Aniva	495ea1ac14	feat: Environment pickling	2024-11-08 14:49:49 -08:00
Leni Aniva	ee8063e1f5	refactor: Merge all Delation functions	2024-11-08 14:41:24 -08:00
Leni Aniva	70f86f6e93	doc: Update delation documentation	2024-11-08 14:34:15 -08:00
Leni Aniva	0d57027681	refactor: Merge Condensed into Delate	2024-11-08 13:05:48 -08:00
Leni Aniva	1c4f38e5eb	refactor: Rename {Serial,Delate}.lean	2024-11-08 13:04:00 -08:00
Leni Aniva	d7c9590780	feat: Extract used constants from invocation	2024-11-05 14:37:06 -08:00
Leni Aniva	645d9c9250	feat: Let tactic in REPL	2024-10-12 16:17:21 -07:00
Leni Aniva	641f8c3883	fix: Translate level mvars	2024-10-09 15:49:10 -07:00
Leni Aniva	0e8c9f890b	fix: Translate fvars in pending context	2024-10-08 14:28:35 -07:00
Leni Aniva	420e863756	fix: Delayed mvars in MetaTranslate	2024-10-08 10:32:16 -07:00
Leni Aniva	25dd1a32ba	Merge branch 'dev' into misc/version	2024-10-06 16:12:36 -07:00
Leni Aniva	9119f47a8f	chore: Remove more thin wrappers	2024-10-06 16:12:22 -07:00
Leni Aniva	8d774d3281	feat: Remove most filters on catalog	2024-10-06 16:12:22 -07:00
Leni Aniva	c3076cbb7d	chore: Update Lean to v4.12.0	2024-10-06 16:10:18 -07:00
Leni Aniva	d0321e72dd	feat: Add message diagnostics to frontend.process	2024-10-05 14:49:17 -07:00
Leni Aniva	10cb32e03f	Merge branch 'dev' into frontend/collect-holes	2024-10-03 11:47:38 -07:00
Leni Aniva	a03eeddc9b	fix: Variable duplication in nested translation	2024-10-03 11:46:09 -07:00
Leni Aniva	530a1a1a97	fix: Extracting `sorry`s from coupled goals	2024-10-03 11:35:54 -07:00
Leni Aniva	ed1f96d7f7	Merge branch 'dev' into goal/tactic	2024-10-03 01:38:10 -07:00
Leni Aniva	143cd289bb	fix: Extraction of sorry's from nested tactics	2024-10-03 01:29:46 -07:00
Leni Aniva	18cd1d0388	fix: Extracting sorrys from sketches	2024-10-02 22:22:20 -07:00
Leni Aniva	fe8b259e4f	feat: Set root when there's just one mvar	2024-09-09 17:37:59 -07:00
Leni Aniva	f729a357b9	Merge branch 'dev' into frontend/collect-holes	2024-09-09 17:35:10 -07:00
Leni Aniva	9075ded885	feat: Set `automaticMode` to true by default	2024-09-09 17:29:43 -07:00
Leni Aniva	762a139e78	feat: Export frontend functions	2024-09-09 12:30:32 -07:00
Leni Aniva	4f5950ed78	feat: Convert holes to goals	2024-09-09 12:26:46 -07:00
Leni Aniva	08fb53c020	test: Frontend process testing	2024-09-09 10:18:20 -07:00
Leni Aniva	8e3241c02a	refactor: Move all frontend functions to `Frontend`	2024-09-08 15:02:43 -07:00
Leni Aniva	5e99237e09	fix: Tactics should produce `.syntheticOpaque` goals	2024-09-08 14:13:39 -07:00
Leni Aniva	860344f9c5	refactor: Factor out `FrontendM` driver	2024-09-08 13:44:46 -07:00
Leni Aniva	b645d79fda	Merge branch 'dev' into goal/automatic	2024-09-08 12:13:42 -07:00
Leni Aniva	7c49fcff27	refactor: Un-export two field accessor functions ... User should use `lean_ctor_get`	2024-09-08 11:53:54 -07:00
Leni Aniva	68dac4c951	chore: Version bump to 0.2.18	2024-09-07 13:55:41 -07:00
Leni Aniva	4042ec707e	refactor: Use `Meta.mapMetaM`	2024-09-07 13:54:52 -07:00
Leni Aniva	8394e1b468	feat: Expose `conv` and `calc` tactics	2024-09-07 13:47:55 -07:00
Leni Aniva	a7b30af36b	refactor: Refactor REPL out of main library ... fix: Calc previous rhs not found bug	2024-09-06 22:01:36 -07:00
Leni Aniva	37473b3efb	feat: Automatic mode (auto resume)	2024-09-06 21:30:11 -07:00
Leni Aniva	82d99ccf9b	refactor: Use `MVarId` across the board	2024-09-06 21:07:12 -07:00
Leni Aniva	02556f3c79	feat: Expose `GoalState` functions	2024-09-05 11:56:06 -07:00
Leni Aniva	9c40a83956	fix: Instantiate type when detecting `eq`	2024-09-03 19:05:16 -07:00
Leni Aniva	f8df2599f9	fix: Use `replaceMainGoal` instead of `setGoals`	2024-09-03 14:18:47 -07:00
Leni Aniva	8d2cd6dfc7	fix: Bindings in prograde tactics	2024-09-03 14:15:52 -07:00
Leni Aniva	edec0f5733	feat: Use CoreM for diag monad	2024-08-26 13:42:14 -04:00
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