command ::= ... |declModifiers class
`declModifiers` is the collection of modifiers on a declaration: * a doc comment `/-- ... -/` * a list of attributes `@[attr1, attr2]` * a visibility specifier, `private`, `protected`, or `public` * `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.
declId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
bracketedBinder* (: term)? (extends (ident : )?term,*)? where (
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
declModifiers ident ::)? structFields (deriving ident,*)?
`declModifiers` is the collection of modifiers on a declaration: * a doc comment `/-- ... -/` * a list of attributes `@[attr1, attr2]` * a visibility specifier, `private`, `protected`, or `public` * `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.
Declares a new type class.