Skip to content

[Feature] Multilean support #325

@pimotte

Description

@pimotte

Currently, the multilean directives in lean-based files are just ignored. We should implement support for this.

Acceptance criteria:

  • Mathgroup block is available in waterproof-editor
  • Waterproof-vscode configures a button to use this for Lean files

Metadata

Metadata

Assignees

Labels

requestRequest for a new feature

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions