The project should export a Rudolf component that takes the parameters necessary to set up a single exercise (i.e. a set of formulas and possibly also a statement that is proved if the tree closes), plus a checker callback.
The additional apparatus which supports the live demo (including the premise input, prebuilt Carnap code) should be decoupled from the core component.
The project should export a Rudolf component that takes the parameters necessary to set up a single exercise (i.e. a set of formulas and possibly also a statement that is proved if the tree closes), plus a checker callback.
The additional apparatus which supports the live demo (including the premise input, prebuilt Carnap code) should be decoupled from the core component.