293 Commits

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