command ::= ...
| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`
All modifiers are optional, and have to come in the listed order.
`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.
declModifiers
example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
optDeclSig := termTermination hints are `termination_by` and `decreasing_by`, in that order.
command ::= ...
| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`
All modifiers are optional, and have to come in the listed order.
`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.
declModifiers
example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
optDeclSig
(| term => term)*Termination hints are `termination_by` and `decreasing_by`, in that order.
command ::= ...
| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`
All modifiers are optional, and have to come in the listed order.
`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.
declModifiers
example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
optDeclSig where
structInstField*