Skip to content

Feature: Easier create exercise #362

Description

@raulTUe

Issue #307 has been split off into two to accommodate the usage of multilean. This feature request focuses on exclusively the create exercise button, a button that allows a teacher to create an exercise for their worksheet with the following structure at the click of a button:

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
```
::::

Metadata

Metadata

Assignees

Labels

requestRequest for a new feature
No fields configured for Feature.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions