152 Commits

Author	SHA1	Message	Date
Leni Aniva	8d774d3281	feat: Remove most filters on catalog	2024-10-06 16:12:22 -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	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	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	25bb964604	test: Automatic mode testing ... refactor: Simplified integration test structure	2024-09-08 11:57:39 -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	82d99ccf9b	refactor: Use `MVarId` across the board	2024-09-06 21:07:12 -07:00
Leni Aniva	8d2cd6dfc7	fix: Bindings in prograde tactics	2024-09-03 14:15:52 -07:00
Leni Aniva	43e11f1ba3	refactor: Always display isInaccessible	2024-08-17 00:53:38 -07:00
Leni Aniva	e1b7eaab12	fix: Let tactic not bringing binder into scope	2024-08-17 00:47:12 -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	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	431ca4e481	fix: Move elab context to condensed	2024-07-22 17:57:01 -07:00
Leni Aniva	6ddde2963d	test: Eval instantiate	2024-06-27 14:51:16 -04:00
Leni Aniva	fc0d872343	refactor: Simplify proof test infrastructure	2024-06-27 14:34:21 -04:00
Leni Aniva	58f9d72288	test: Evaluate tactic context	2024-06-25 16:18:31 -04:00
Leni Aniva	c0124b347f	Merge branch 'serial/expr' into tactic/eval	2024-06-25 16:05:20 -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	f80d90ce87	fix: Goal diag missing newline character	2024-06-14 11:59:02 -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	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