# Documentation

Lean.Elab.StructInst

Instances For

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

Instances For
Instances For
• implicit :
Instances For
Instances For
• fieldName:
• fieldIndex:
• modifyOp:
Instances For
• term:
• nested: {σ : Type} →
• default:
Instances For
Instances For
Instances For
• mk:

Remark: the field params is use for default value propagation. It is initially empty, and then set at elabStruct.

Instances For
@[inline, reducible]
Instances For
Instances For
Instances For

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

Instances For
Instances For
Instances For
Instances For
Instances For
def Lean.Elab.Term.StructInst.mkProjStx? (s : Lean.Syntax) (structName : Lake.Name) (fieldName : Lake.Name) :
Instances For
Instances For
Instances For
Instances For
Instances For
def Lean.Elab.Term.StructInst.throwFailedToElabField {α : Type} (fieldName : Lake.Name) (structName : Lake.Name) (msgData : Lean.MessageData) :
Instances For
Instances For
• structs :
• allStructNames :
• maxDistance : Nat

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).
Instances For
Instances For
Instances For
Instances For
@[inline, reducible]
Instances For
Instances For
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 : Lake.Name) (mvarId : Lean.MVarId) :
Instances For
partial def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : ) (allStructNames : ) (maxDistance : Nat) (fieldName : Lake.Name) (mvarId : Lean.MVarId) (i : Nat) (dist : Nat) :
Instances For
Instances For