def Lean.Elab.Term.StructInst.expandStructInstExpectedType : Lean.Macro

def Lean.Elab.Term.StructInst.expandStructInstFieldAbbrev : Lean.Macro

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

structure Lean.Elab.Term.StructInst.ExplicitSourceInfo : Type

• stx : Lean.Syntax
• structName : Lake.Name

instance Lean.Elab.Term.StructInst.instInhabitedExplicitSourceInfo : Inhabited Lean.Elab.Term.StructInst.ExplicitSourceInfo

structure Lean.Elab.Term.StructInst.Source : Type

• explicit : Array Lean.Elab.Term.StructInst.ExplicitSourceInfo
• implicit : Option Lean.Syntax

instance Lean.Elab.Term.StructInst.instInhabitedSource : Inhabited Lean.Elab.Term.StructInst.Source

def Lean.Elab.Term.StructInst.Source.isNone : Lean.Elab.Term.StructInst.Source → Bool

inductive Lean.Elab.Term.StructInst.FieldLHS : Type

• fieldName: Lean.Syntax → Lake.Name → Lean.Elab.Term.StructInst.FieldLHS
• fieldIndex: Lean.Syntax → Nat → Lean.Elab.Term.StructInst.FieldLHS
• modifyOp: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.StructInst.FieldLHS

instance Lean.Elab.Term.StructInst.instInhabitedFieldLHS : Inhabited Lean.Elab.Term.StructInst.FieldLHS

instance Lean.Elab.Term.StructInst.instToFormatFieldLHS : Lean.ToFormat Lean.Elab.Term.StructInst.FieldLHS

inductive Lean.Elab.Term.StructInst.FieldVal (σ : Type) : Type

• term: {σ : Type} → Lean.Syntax → Lean.Elab.Term.StructInst.FieldVal σ
• nested: {σ : Type} → σ → Lean.Elab.Term.StructInst.FieldVal σ
• default: {σ : Type} → Lean.Elab.Term.StructInst.FieldVal σ

instance Lean.Elab.Term.StructInst.instInhabitedFieldVal : {a : Type} → Inhabited (Lean.Elab.Term.StructInst.FieldVal a)

structure Lean.Elab.Term.StructInst.Field (σ : Type) : Type

• ref : Lean.Syntax
• lhs : List Lean.Elab.Term.StructInst.FieldLHS
• val : Lean.Elab.Term.StructInst.FieldVal σ
• expr? : Option Lean.Expr

instance Lean.Elab.Term.StructInst.instInhabitedField : {a : Type} → Inhabited (Lean.Elab.Term.StructInst.Field a)

def Lean.Elab.Term.StructInst.Field.isSimple {σ : Type} : Lean.Elab.Term.StructInst.Field σ → Bool

inductive Lean.Elab.Term.StructInst.Struct : Type

• mk: Lean.Syntax → Lake.Name → Array (Lake.Name × Lean.Expr) → List (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) → Lean.Elab.Term.StructInst.Source → Lean.Elab.Term.StructInst.Struct

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

instance Lean.Elab.Term.StructInst.instInhabitedStruct : Inhabited Lean.Elab.Term.StructInst.Struct

@[inline, reducible]

abbrev Lean.Elab.Term.StructInst.Fields : Type

def Lean.Elab.Term.StructInst.Struct.ref : Lean.Elab.Term.StructInst.Struct → Lean.Syntax

def Lean.Elab.Term.StructInst.Struct.structName : Lean.Elab.Term.StructInst.Struct → Lake.Name

def Lean.Elab.Term.StructInst.Struct.params : Lean.Elab.Term.StructInst.Struct → Array (Lake.Name × Lean.Expr)

def Lean.Elab.Term.StructInst.Struct.fields : Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Fields

def Lean.Elab.Term.StructInst.Struct.source : Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Source

partial def Lean.Elab.Term.StructInst.Struct.allDefault (s : Lean.Elab.Term.StructInst.Struct) : Bool

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

def Lean.Elab.Term.StructInst.formatField (formatStruct : Lean.Elab.Term.StructInst.Struct → Lean.Format) (field : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) : Lean.Format

partial def Lean.Elab.Term.StructInst.formatStruct : Lean.Elab.Term.StructInst.Struct → Lean.Format

instance Lean.Elab.Term.StructInst.instToFormatStruct : Lean.ToFormat Lean.Elab.Term.StructInst.Struct

instance Lean.Elab.Term.StructInst.instToStringStruct : ToString Lean.Elab.Term.StructInst.Struct

instance Lean.Elab.Term.StructInst.instToFormatFieldStruct : Lean.ToFormat (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

instance Lean.Elab.Term.StructInst.instToStringFieldStruct : ToString (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

def Lean.Elab.Term.StructInst.FieldLHS.toSyntax (first : Bool) : Lean.Elab.Term.StructInst.FieldLHS → Lean.Syntax

def Lean.Elab.Term.StructInst.FieldVal.toSyntax : Lean.Elab.Term.StructInst.FieldVal Lean.Elab.Term.StructInst.Struct → Lean.Syntax

def Lean.Elab.Term.StructInst.Field.toSyntax : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct → Lean.Syntax

def Lean.Elab.Term.StructInst.Struct.modifyFieldsM {m : Type → Type} [Monad m] (s : Lean.Elab.Term.StructInst.Struct) (f : Lean.Elab.Term.StructInst.Fields → m Lean.Elab.Term.StructInst.Fields) : m Lean.Elab.Term.StructInst.Struct

def Lean.Elab.Term.StructInst.Struct.modifyFields (s : Lean.Elab.Term.StructInst.Struct) (f : Lean.Elab.Term.StructInst.Fields → Lean.Elab.Term.StructInst.Fields) : Lean.Elab.Term.StructInst.Struct

def Lean.Elab.Term.StructInst.Struct.setFields (s : Lean.Elab.Term.StructInst.Struct) (fields : Lean.Elab.Term.StructInst.Fields) : Lean.Elab.Term.StructInst.Struct

def Lean.Elab.Term.StructInst.Struct.setParams (s : Lean.Elab.Term.StructInst.Struct) (ps : Array (Lake.Name × Lean.Expr)) : Lean.Elab.Term.StructInst.Struct

def Lean.Elab.Term.StructInst.mkProjStx? (s : Lean.Syntax) (structName : Lake.Name) (fieldName : Lake.Name) : Lean.Elab.TermElabM (Option Lean.Syntax)

def Lean.Elab.Term.StructInst.findField? (fields : Lean.Elab.Term.StructInst.Fields) (fieldName : Lake.Name) : Option (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

structure Lean.Elab.Term.StructInst.CtorHeaderResult : Type

• ctorFn : Lean.Expr
• ctorFnType : Lean.Expr
• instMVars : Array Lean.MVarId
• params : Array (Lake.Name × Lean.Expr)

def Lean.Elab.Term.StructInst.markDefaultMissing (e : Lean.Expr) : Lean.Expr

def Lean.Elab.Term.StructInst.defaultMissing? (e : Lean.Expr) : Option Lean.Expr

def Lean.Elab.Term.StructInst.throwFailedToElabField {α : Type} (fieldName : Lake.Name) (structName : Lake.Name) (msgData : Lean.MessageData) : Lean.Elab.TermElabM α

def Lean.Elab.Term.StructInst.trySynthStructInstance? (s : Lean.Elab.Term.StructInst.Struct) (expectedType : Lean.Expr) : Lean.Elab.TermElabM (Option Lean.Expr)

structure Lean.Elab.Term.StructInst.ElabStructResult : Type

• val : Lean.Expr
• struct : Lean.Elab.Term.StructInst.Struct
• instMVars : Array Lean.MVarId

structure Lean.Elab.Term.StructInst.DefaultFields.Context : Type

• structs : Array Lean.Elab.Term.StructInst.Struct
• allStructNames : Array Lake.Name
• 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).

structure Lean.Elab.Term.StructInst.DefaultFields.State : Type

• progress : Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.collectStructNames (struct : Lean.Elab.Term.StructInst.Struct) (names : Array Lake.Name) : Array Lake.Name

partial def Lean.Elab.Term.StructInst.DefaultFields.getHierarchyDepth (struct : Lean.Elab.Term.StructInst.Struct) : Nat

def Lean.Elab.Term.StructInst.DefaultFields.isDefaultMissing? {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (field : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) : m Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.findDefaultMissing? {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.Struct) : m (Option (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct))

def Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.Struct) : m (Array (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct))

partial def Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing.go {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.Struct) : StateT (Array (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)) m Unit

def Lean.Elab.Term.StructInst.DefaultFields.getFieldName (field : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) : Lake.Name

@[inline, reducible]

abbrev Lean.Elab.Term.StructInst.DefaultFields.M (α : Type) : Type

def Lean.Elab.Term.StructInst.DefaultFields.isRoundDone : Lean.Elab.Term.StructInst.DefaultFields.M Bool

def Lean.Elab.Term.StructInst.DefaultFields.getFieldValue? (struct : Lean.Elab.Term.StructInst.Struct) (fieldName : Lake.Name) : Option Lean.Expr

partial def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValueAux? (struct : Lean.Elab.Term.StructInst.Struct) : Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)

def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValue? (struct : Lean.Elab.Term.StructInst.Struct) (cinfo : Lean.ConstantInfo) : Lean.Elab.TermElabM (Option Lean.Expr)

partial def Lean.Elab.Term.StructInst.DefaultFields.reduce (structNames : Array Lake.Name) (e : Lean.Expr) : Lean.MetaM Lean.Expr

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

def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault (structs : Array Lean.Elab.Term.StructInst.Struct) (allStructNames : Array Lake.Name) (maxDistance : Nat) (fieldName : Lake.Name) (mvarId : Lean.MVarId) : Lean.Elab.TermElabM Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : Array Lean.Elab.Term.StructInst.Struct) (allStructNames : Array Lake.Name) (maxDistance : Nat) (fieldName : Lake.Name) (mvarId : Lean.MVarId) (i : Nat) (dist : Nat) : Lean.Elab.TermElabM Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.step (struct : Lean.Elab.Term.StructInst.Struct) : Lean.Elab.Term.StructInst.DefaultFields.M Unit

partial def Lean.Elab.Term.StructInst.DefaultFields.propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Lean.Elab.Term.StructInst.Struct) : Lean.Elab.Term.StructInst.DefaultFields.M Unit

def Lean.Elab.Term.StructInst.DefaultFields.propagate (struct : Lean.Elab.Term.StructInst.Struct) : Lean.Elab.TermElabM Unit

def Lean.Elab.Term.StructInst.elabStructInst : Lean.Elab.Term.TermElab