140 Commits

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