command ::= ... |declModifiers
declModifiers
is the collection of modifiers on a declaration:
- a doc comment
/-- ... -/
- a list of attributes
@[attr1, attr2]
- a visibility specifier,
private
orprotected
noncomputable
unsafe
partial
ornonrec
All modifiers are optional, and have to come in the listed order.
nestedDeclModifiers
is the same asdeclModifiers
, 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, andlet rec
/where
definitions.inductive
In Lean, every concrete type other than the universes and every type constructor other than dependent arrows is an instance of a general family of type constructions known as inductive types. It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, dependent arrow types, and inductive types; everything else follows from those. Intuitively, an inductive type is built up from a specified list of constructors. For example,
List α
is the list of elements of typeα
, and is defined as follows:inductive List (α : Type u) where | nil | cons (head : α) (tail : List α)
A list of elements of type
α
is either the empty list,nil
, or an elementhead : α
followed by a listtail : List α
. See Inductive types for more information.declId
declId
matchesfoo
orfoo.{u,v}
: an identifier possibly followed by a list of universe namesoptDeclSig where (|
optDeclSig
matches the signature of a declaration with optional type: a list of binders and then possibly: type
declModifiers ident
declModifiers
is the collection of modifiers on a declaration:
- a doc comment
/-- ... -/
- a list of attributes
@[attr1, attr2]
- a visibility specifier,
private
orprotected
noncomputable
unsafe
partial
ornonrec
All modifiers are optional, and have to come in the listed order.
nestedDeclModifiers
is the same asdeclModifiers
, 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, andlet rec
/where
definitions.optDeclSig)* (deriving ident,*)?
optDeclSig
matches the signature of a declaration with optional type: a list of binders and then possibly: type
新しい帰納型を宣言します。 declModifiers
の意味は 宣言修飾子について の節で説明した通りです。