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 |
Leni Aniva
|
8e78718447
|
feat: Extract MetaM context and state from goal
|
2024-06-25 15:54:55 -04:00 |
Leni Aniva
|
ffbea41f62
|
feat: Condensed interface
|
2024-06-25 15:13:58 -04:00 |