Structure instance elaborator #
A structure instance is notation to construct a term of a structure.
Examples: { x := 2, y.z := true }, { s with cache := c' }, and { s with values[2] := v }.
Structure instances are the preferred way to invoke a structure's constructor,
since they hide Lean implementation details such as whether parents are represented as subobjects,
and also they do correct processing of default values,
which are complicated due to the fact that structures can override default values of their parents,
and furthermore overridden default values can use fields that come after in the order the fields appear in the constructor.
This module elaborates structure instance notation.
Note that the where syntax to define structures (Lean.Parser.Command.whereStructInst)
macro expands into the structure instance notation elaborated by this module.
Recall that structure instances are (after removing parsing and pretty printing hints):
def structInst := leading_parser
"{ " >> optional (sepBy1 termParser ", " >> " with ")
>> structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
>> optEllipsis
>> optional (" : " >> termParser) >> " }"
def structInstField := leading_parser
structInstLVal >> optional (many structInstFieldBinder >> optType >> structInstFieldDecl)
@[builtin_structInstFieldDecl_parser]
def structInstFieldDef := leading_parser
" := " >> termParser
@[builtin_structInstFieldDecl_parser]
def structInstFieldEqns := leading_parser
matchAlts
def structInstWhereBody := leading_parser
structInstFields (sepByIndent structInstField "; " (allowTrailingSep := true))
@[builtin_structInstFieldDecl_parser]
def structInstFieldWhere := leading_parser
"where" >> structInstWhereBody
Transforms structure instances such as { x := 0 : Foo } into ({ x := 0 } : Foo).
Structure instance notation makes use of the expected type.
Equations
- One or more equations did not get rendered due to their size.
Expands fields.
- Abbrevations. Example:
{ x }expands to{ x := x }. - Equations. Example:
{ f | 0 => 0 | n + 1 => n }expands to{ f := fun x => match x with | 0 => 0 | n + 1 => n }. - Binders and types. Example:
{ f n : Nat := n + 1 }expands to{ f := fun n => (n + 1 : Nat) }.
Equations
- One or more equations did not get rendered due to their size.
An explicit source is one of the structures sᵢ that appear in { s₁, …, sₙ with … }.
Equations
- Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView = { default := { stx := default, fvar := default, structName := default } }
A view of the sources of fields for the structure instance notation.
- explicit : Array ExplicitSourceView
Explicit sources (i.e., one of the structures
sᵢthat appear in{ s₁, …, sₙ with … }). The syntax for a trailing
... This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications.
Instances For
Equations
- Lean.Elab.Term.StructInst.instInhabitedSourcesView = { default := { explicit := default, implicit := default } }
A component of a left-hand side for a field appearing in structure instance syntax.
- fieldName
(ref : Syntax)
(name : Name)
: FieldLHS
A name component for a field left-hand side. For example,
xandyin{ x.y := v }. - parentFieldName
(ref : Syntax)
(structName name : Name)
: FieldLHS
(Can't be written by users.) A field setting an entire parent. The
structNameis the name of the parent structure, andnameis the projection field name. Always appears as the only LHS component. - fieldIndex
(ref : Syntax)
(idx : Nat)
: FieldLHS
A numeric index component for a field left-hand side. For example
3in{ x.3 := v }. - modifyOp
(ref index : Syntax)
: FieldLHS
An array indexing component for a field left-hand side. For example
[3]in{ arr[3] := v }.
Equations
- One or more equations did not get rendered due to their size.
Field StructInstView is a representation of a field in the structure instance.
Equations
- Lean.Elab.Term.StructInst.instInhabitedFieldView = { default := { ref := default, lhs := default, val := default } }
The view for structure instance notation.
- ref : Syntax
The syntax for the whole structure instance.
The fields of the structure instance.
- sources : SourcesView
The additional sources for fields for the structure instance.
Equations
- Lean.Elab.Term.StructInst.instInhabitedStructInstView = { default := { ref := default, fields := default, sources := default } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.