Definitions that use := associate the term on the right-hand side with the constant's name.
The term is wrapped in a Lean.Parser.Term.fun : termfun for each parameter, and the type is found by binding the parameters in a function type.
Definitions with def are semireducible.
command ::= ... |declModifiers def`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 namesoptDeclSig := term`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`Termination hints are `termination_by` and `decreasing_by`, in that order.
Definitions may use pattern matching.
These definitions are desugared to uses of Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match.
command ::= ... |declModifiers def`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 namesoptDeclSig (| term => term)*`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`Termination hints are `termination_by` and `decreasing_by`, in that order.
Values of structure types, or functions that return them, may be defined by providing values for their fields, following where:
command ::= ... |declModifiers def`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 namesoptDeclSig where structInstField*`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
