Description

The AST could be expanded such that more complex notations could be represented.
A new constructor for notations should be added where the left hand side is not a single notation identifier but a list of notation and variable identifiers and the right hand side has an additional list of syntax modifiers.

Motivation

To solve an issue #153 for the free-compiler, I need to be able to define smart constructors as notations like the following.

Notation "'Cons' x xs" := (pure (cons x xs))
  (at level 10, x, xs at level 9).

The current representation however only supports notations of the following form.

Notation "'ident'" := (term).

It cannot have identifiers in the notation string for variables and any syntax modifiers.

Alternatives

The simplest notation expansion that solves my problem would be to support abbreviations.

Notation Cons x xs := (pure (cons x xs)).

This solution however requires that the smart constructor name is a valid identifier and it would not be possible to define for example what @Cons means. The solution above would allow this.

Notation "'@Cons' Shape Pos a x xs" := (@pure Shape Pos (List Shape Pos a) (@cons Shape Pos a x xs))
  (at level 10, Shape, Pos, a, x, xs at level 9, only parsing).

Additional Context

Description

Add the possibility to add Context commands to sections.

Motivation

Alternatives

Additional Context

Description

Coq provides several flags and options but there are currently no sentences in this AST to use them.

Motivation

Alternatives

This issue needs to unset a flag to define an induction schemes with the correct naming scheme.

Additional Context

Description

Add the possibility to add hints to a hint database in Coq.

Motivation

Hint databases are very useful for automatically building proofs. They need however to be filled with hints which is not possible with the current representation of Coq.

Alternatives

Additional Context