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

Equations

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

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

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.

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

Equations

• Lean.Elab.Term.StructInst.instInhabitedExplicitSourceInfo = { default := { stx := default, structName := default } }

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

Equations

• Lean.Elab.Term.StructInst.instInhabitedSource = { default := { explicit := default, implicit := default } }

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

Equations

• x.isNone = match x with | { explicit := #[], implicit := none } => true | x => false

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

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldLHS = { default := Lean.Elab.Term.StructInst.FieldLHS.fieldName default default }

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

Equations

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

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)

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldVal = { default := Lean.Elab.Term.StructInst.FieldVal.term default }

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)

Equations

• Lean.Elab.Term.StructInst.instInhabitedField = { default := { ref := default, lhs := default, val := default, expr? := default } }

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

Equations

• { ref := ref, lhs := [head], val := val, expr? := expr? }.isSimple = true
• x.isSimple = false

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

Equations

• Lean.Elab.Term.StructInst.instInhabitedStruct = { default := Lean.Elab.Term.StructInst.Struct.mk default default default default default }

@[reducible, inline]

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

Equations

• Lean.Elab.Term.StructInst.Fields = List (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).ref = ref

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).structName = structName

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).params = params

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).fields = fields

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).source = 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

Equations

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

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

Equations

• Lean.Elab.Term.StructInst.instToFormatStruct = { format := Lean.Elab.Term.StructInst.formatStruct }

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

Equations

• Lean.Elab.Term.StructInst.instToStringStruct = { toString := toString ∘ Lean.format }

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

Equations

• Lean.Elab.Term.StructInst.instToFormatFieldStruct = { format := Lean.Elab.Term.StructInst.formatField Lean.Elab.Term.StructInst.formatStruct }

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

Equations

• Lean.Elab.Term.StructInst.instToStringFieldStruct = { toString := toString ∘ Lean.format }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.StructInst.FieldLHS.toSyntax first (Lean.Elab.Term.StructInst.FieldLHS.modifyOp stx index) = stx
• Lean.Elab.Term.StructInst.FieldLHS.toSyntax first (Lean.Elab.Term.StructInst.FieldLHS.fieldIndex stx idx) = if first = true then stx else Lean.mkGroupNode #[Lean.mkAtomFrom stx ".", stx]

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

Equations

• (Lean.Elab.Term.StructInst.FieldVal.term stx).toSyntax = stx
• x.toSyntax = panicWithPosWithDecl "Lean.Elab.StructInst" "Lean.Elab.Term.StructInst.FieldVal.toSyntax" 336 25 "unreachable code has been reached"

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

Equations

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

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

Equations

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

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

Equations

• s.modifyFields f = (s.modifyFieldsM f).run

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

Equations

• s.setFields fields = s.modifyFields fun (x : Lean.Elab.Term.StructInst.Fields) => fields

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

Equations

• (Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source).setParams ps = Lean.Elab.Term.StructInst.Struct.mk ref structName ps fields source

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

Equations

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

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)

Equations

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

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

Equations

• Lean.Elab.Term.StructInst.markDefaultMissing e = Lean.mkAnnotation `structInstDefault e

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

Equations

• Lean.Elab.Term.StructInst.defaultMissing? e = Lean.annotation? `structInstDefault e

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

Equations

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

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

Equations

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

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

Equations

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

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))

Equations

• Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing struct = (SeqRight.seqRight (Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing.go struct) fun (x : Unit) => get).run' #[]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Elab.Term.StructInst.DefaultFields.M = ReaderT Lean.Elab.Term.StructInst.DefaultFields.Context (StateRefT' IO.RealWorld Lean.Elab.Term.StructInst.DefaultFields.State Lean.Elab.TermElabM)

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

Equations

• Lean.Elab.Term.StructInst.DefaultFields.isRoundDone = do let __do_lift ← get let __do_lift_1 ← read pure (__do_lift.progress && decide (__do_lift_1.maxDistance > 0))

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

Equations

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

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)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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