Lean.Elab.StructInst

Structure instances are of the form:

  "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
      >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
      >> optEllipsis
      >> optional (" : " >> termParser)
      >> " }"

Equations

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

source

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.

source

structure Lean.Elab.Term.StructInst.ExplicitSourceInfo:

Type

stx : Lean.Syntax
structName : Lean.Name

source

instance Lean.Elab.Term.StructInst.instInhabitedExplicitSourceInfo:

Inhabited Lean.Elab.Term.StructInst.ExplicitSourceInfo

Equations

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

source

inductive Lean.Elab.Term.StructInst.Source:

Type

none: Lean.Elab.Term.StructInst.Source
implicit: Lean.Syntax → Lean.Elab.Term.StructInst.Source
explicit: Array Lean.Elab.Term.StructInst.ExplicitSourceInfo → Lean.Elab.Term.StructInst.Source

source

instance Lean.Elab.Term.StructInst.instInhabitedSource:

Inhabited Lean.Elab.Term.StructInst.Source

Equations

Lean.Elab.Term.StructInst.instInhabitedSource = { default := Lean.Elab.Term.StructInst.Source.none }

source

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

Lean.Elab.Term.StructInst.Source → Bool

Equations

Lean.Elab.Term.StructInst.Source.isNone _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Source.none => true | x => false

source

inductive Lean.Elab.Term.StructInst.FieldLHS:

Type

fieldName: Lean.Syntax → Lean.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

source

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 }

source

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.

source

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 σ

source

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 }

source

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

source

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

source

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

Lean.Elab.Term.StructInst.Field σ → Bool

Equations

Lean.Elab.Term.StructInst.Field.isSimple _fun_discr = match _fun_discr with | { ref := ref, lhs := [head], val := val, expr? := expr? } => true | x => false

source

inductive Lean.Elab.Term.StructInst.Struct:

Type

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

source

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 }

source

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

source

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

Lean.Elab.Term.StructInst.Struct → Lean.Syntax

Equations

Lean.Elab.Term.StructInst.Struct.ref _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source => ref

source

def Lean.Elab.Term.StructInst.Struct.structName:

Lean.Elab.Term.StructInst.Struct → Lean.Name

Equations

Lean.Elab.Term.StructInst.Struct.structName _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source => structName

source

def Lean.Elab.Term.StructInst.Struct.params:

Lean.Elab.Term.StructInst.Struct → Array (Lean.Name × Lean.Expr)

Equations

Lean.Elab.Term.StructInst.Struct.params _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source => params

source

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

Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Fields

Equations

Lean.Elab.Term.StructInst.Struct.fields _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Struct.mk ref structName params fields source => fields

source

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

Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Source

Equations

Lean.Elab.Term.StructInst.Struct.source _fun_discr = match _fun_discr with | Lean.Elab.Term.StructInst.Struct.mk ref structName params fields s => s

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

source

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.

source

partial def Lean.Elab.Term.StructInst.formatStruct:

Lean.Elab.Term.StructInst.Struct → Lean.Format

source

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 }

source

instance Lean.Elab.Term.StructInst.instToStringStruct:

ToString Lean.Elab.Term.StructInst.Struct

Equations

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

source

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 }

source

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 }

source

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.

source

def Lean.Elab.Term.StructInst.FieldVal.toSyntax:

Lean.Elab.Term.StructInst.FieldVal Lean.Elab.Term.StructInst.Struct → Lean.Syntax

Equations

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

source

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.

source

def Lean.Elab.Term.StructInst.Struct.modifyFieldsM {m : Type → Type} [inst : 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.

source

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

Lean.Elab.Term.StructInst.Struct.modifyFields s f = Id.run (Lean.Elab.Term.StructInst.Struct.modifyFieldsM s f)

source

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

Lean.Elab.Term.StructInst.Struct.setFields s fields = Lean.Elab.Term.StructInst.Struct.modifyFields s fun x => fields

source

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

Lean.Elab.Term.StructInst.Struct

Equations

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

source

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

Lean.Elab.TermElabM (Option Lean.Syntax)

Equations

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

source

def Lean.Elab.Term.StructInst.findField? (fields : Lean.Elab.Term.StructInst.Fields) (fieldName : Lean.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.

source

structure Lean.Elab.Term.StructInst.CtorHeaderResult:

Type

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

source

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

Lean.Expr

Equations

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

source

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

Option Lean.Expr

Equations

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

source

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

Lean.Elab.TermElabM α

Equations

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

source

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.

source

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

Type

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

source

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

Type

progress : Bool

source

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

Array Lean.Name

source

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

Nat

source

partial def Lean.Elab.Term.StructInst.DefaultFields.findDefaultMissing? (mctx : Lean.MetavarContext) (struct : Lean.Elab.Term.StructInst.Struct) :

Option (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

source

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

Lean.Name

Equations

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

source

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

source

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

Lean.Elab.Term.StructInst.DefaultFields.M Bool

Equations

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

source

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

Option Lean.Expr

Equations

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

source

partial def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValueAux? (struct : Lean.Elab.Term.StructInst.Struct) :

Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)

source

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.

source

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

Lean.MetaM Lean.Expr

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

source

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

Lean.Elab.TermElabM Bool

Equations

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

source

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

Lean.Elab.TermElabM Bool

source

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

Lean.Elab.Term.StructInst.DefaultFields.M Unit

source

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

source

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.

source

def Lean.Elab.Term.StructInst.elabStructInst:

Lean.Elab.Term.TermElab

Structure instance. { x := e, ... } assigns e to field x, which may be inherited. If e is itself a variable called x, it can be elided: fun y => { x := 1, y }. A structure update of an existing value can be given via with: { point with x := 1 }. The structure type can be specified if not inferable: { x := 1, y := 2 : Point }.

Equations

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