The syntax of theorems is like that of definitions, except the codomain (that is, the theorem statement) in the signature is mandatory.
command ::= ... |declModifiers theorem
`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.
declId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig := term
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
command ::= ... |declModifiers theorem
`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.
declId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig (| term => term)*
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
command ::= ... |declModifiers theorem
`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.
declId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig where structInstField*
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`