feat: Expose GoalState functions #94

aniva · 2024-09-06T18:06:39-07:00

aniva commented

2024-09-06 18:06:39 -07:00

No description provided.

aniva added 1 commit 2024-09-06 18:06:40 -07:00

02556f3c79

feat: Expose `GoalState` functions

aniva commented

2024-09-06 21:18:28 -07:00

Need to expose the conv and convExit functions as well.

Need to expose the `conv` and `convExit` functions as well.

aniva commented

2024-09-06 23:19:07 -07:00

It is a bit tricky how we can expose the calc tactic. This tactic relies on special data in the goal state object - it isn't a normal Syntax -> TacticM Unit. This data is even used during its expression elaboration. On the other hand, conv is kind of fine, but how are we going to export its tactics?

It is a bit tricky how we can expose the `calc` tactic. This tactic relies on special data in the goal state object - it isn't a normal `Syntax -> TacticM Unit`. This data is even used during its expression elaboration. On the other hand, `conv` is kind of fine, but how are we going to export its tactics?

aniva added 1 commit 2024-09-07 13:48:16 -07:00

8394e1b468

feat: Expose `conv` and `calc` tactics

aniva added 1 commit 2024-09-07 13:55:23 -07:00

4042ec707e

refactor: Use `Meta.mapMetaM`

aniva added the

category

feature

part/FFI

labels 2024-09-07 14:05:21 -07:00

aniva added 1 commit 2024-09-08 11:54:07 -07:00