522 Commits

All Branches

Search

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	e2ad6ce6b3	doc: Documentation for automatic mode	2024-09-06 21:32:02 -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	948b535b5d	Merge pull request 'feat: Prograde tactics' (#83) from tactic/eval into dev ... Reviewed-on: #83	2024-08-31 20:04:38 -07:00
Leni Aniva	edec0f5733	feat: Use CoreM for diag monad	2024-08-26 13:42:14 -04:00
Leni Aniva	0c529c5cd9	Merge branch 'misc/test-driver' into tactic/eval	2024-08-18 12:24:26 -07:00
Leni Aniva	76765c913c	test: Use `lake test`. Retired `Makefile`	2024-08-18 12:22:59 -07: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	5d43068ec3	fix: Flake check failure	2024-08-17 02:07:17 -07:00
Leni Aniva	f87eed817f	build: Move non-package output to legacyPackages	2024-08-17 01:59:48 -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
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	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	56100a30af	Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev ... Reviewed-on: #85	2024-08-15 22:41:58 -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	caac70f0cf	feat: Move non package outputs to dependencies	2024-08-04 17:52:36 -07:00
Leni Aniva	64269868d5	feat: Expose project and leanPkgs in flake	2024-08-04 17:32:20 -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