Currently, the editor buttons all provide relatively elementary operations. In practice, a teacher will create a worksheet consisting of examples and exercises, along with explanatory text and possible hints or "Technical details" sections (i.e. hint sections containing maintainance code).
We want some additional buttons create exercises, examples, texthints and code hints.
Depending on the language, the following snippets should be inserted after the node where the cursor is at the moment of clicking the button.
Create exercise (Rocq):
```coq
Lemma exercise:
Proof.
```
<input-area>
```coq
```
</input-area>
```coq
Qed.
```
Create exercise (Lean):
::::multilean
```lean
Exercise "exercise"
Given:
Assume:
Conclusion:
Proof:
```
:::input
```
:::
```lean
QED
```
::::
Create example (Rocq):
Example example: True.
Proof.
Qed.
Create example (Lean):
Example "example"
Given:
Assume:
Conclusion:
Proof:
QED
Create text hint (Rocq):
<hint title="💡 Hint">
</hint>
Create text hint (Lean)
Create code hint (Rocq):
<hint title="🛠️ Technical details">
```coq
```
</hint>
Create code hint (Lean):
:::hint "🛠️ Technical details"
```lean
```
:::
Currently, the editor buttons all provide relatively elementary operations. In practice, a teacher will create a worksheet consisting of examples and exercises, along with explanatory text and possible hints or "Technical details" sections (i.e. hint sections containing maintainance code).
We want some additional buttons create exercises, examples, texthints and code hints.
Depending on the language, the following snippets should be inserted after the node where the cursor is at the moment of clicking the button.
Create exercise (Rocq):
Create exercise (Lean):
Create example (Rocq):
Create example (Lean):
Example "example" Given: Assume: Conclusion: Proof: QEDCreate text hint (Rocq):
Create text hint (Lean)
Create code hint (Rocq):
Create code hint (Lean):