# Documentation

Lean.Elab.StructInst

Equations
• One or more equations did not get rendered due to their size.

Expand field abbreviations. Example: { x, y := 0 } expands to { x := x, y := 0 }

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• implicit :
Instances For
Equations
Equations
• = match x with | { explicit := #[], implicit := none } => true | x => false
• fieldName:
• fieldIndex:
• modifyOp:
Instances For
Equations
• One or more equations did not get rendered due to their size.
• term:
• nested: {σ : Type} →
• default:
Instances For
Equations
• Lean.Elab.Term.StructInst.instInhabitedFieldVal = { default := }
Instances For
Equations
• Lean.Elab.Term.StructInst.instInhabitedField = { default := { ref := default, lhs := default, val := default, expr? := default } }
Equations
• = match x with | { ref := ref, lhs := [head], val := val, expr? := expr? } => true | x => false
• Remark: the field params is use for default value propagation. It is initially empty, and then set at elabStruct.

mk:
Instances For
Equations
Equations
Equations
Equations
Equations
Equations

true iff all fields of the given structure are marked as default

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
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.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Term.StructInst.mkProjStx? (s : Lean.Syntax) (structName : Lean.Name) (fieldName : Lean.Name) :
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.
Instances For
Equations
Equations
def Lean.Elab.Term.StructInst.throwFailedToElabField {α : Type} (fieldName : Lean.Name) (structName : Lean.Name) (msgData : Lean.MessageData) :
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.
Instances For
• structs :
• allStructNames :
• Consider the following example:

structure A where
x : Nat := 1

structure B extends A where
y : Nat := x + 1
x := y + 1

structure C extends B where
z : Nat := 2*y
x := z + 3


And we are trying to elaborate a structure instance for C. There are default values for x at A, B, and C. We say the default value at C has distance 0, the one at B distance 1, and the one at A distance 2. The field maxDistance specifies the maximum distance considered in a round of Default field computation. Remark: since C does not set a default value of y, the default value at B is at distance 0.

The fixpoint for setting default values works in the following way.

• Keep computing default values using maxDistance == 0.
• We increase maxDistance whenever we failed to compute a new default value in a round.
• If maxDistance > 0, then we interrupt a round as soon as we compute some default value. We use depth-first search.
• We sign an error if no progress is made when maxDistance == structure hierarchy depth (2 in the example above).
maxDistance : Nat
Instances For
Instances For
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
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.
partial def Lean.Elab.Term.StructInst.DefaultFields.reduce (structNames : ) (e : Lean.Expr) :

Reduce default value. It performs beta reduction and projections of the given structures.

def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault (structs : ) (allStructNames : ) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) :
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : ) (allStructNames : ) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) (i : Nat) (dist : Nat) :
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.