Computed fields

Inductives can have computed fields which are recursive functions whose value is stored in the constructors, and can be accessed in constant time.

inductive Exp
  | hole
  | app (x y : Exp)
with
  f : Exp → Nat
    | .hole => 42
    | .app x y => f x + f y

-- `Exp.f x` runs in constant time, even if `x` is a dag-like value

This file implements the computed fields feature by simulating it via implemented_by. The main function is setComputedFields.

opaque Lean.Elab.ComputedFields.computedFieldAttr : TagAttribute

def Lean.Elab.ComputedFields.mkUnsafeCastTo (expectedType e : Expr) : MetaM Expr

Equations

• Lean.Elab.ComputedFields.mkUnsafeCastTo expectedType e = Lean.Meta.mkAppOptM `unsafeCast #[none, some expectedType, some e]

def Lean.Elab.ComputedFields.isScalarField (ctor : Name) : CoreM Bool

Equations

• Lean.Elab.ComputedFields.isScalarField ctor = do let __do_lift ← Lean.getConstInfoCtor ctor pure (__do_lift.numFields == 0)

structure Lean.Elab.ComputedFields.Contextextends Lean.InductiveVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• numParams : Nat
• numIndices : Nat
• all : List Name
• ctors : List Name
• numNested : Nat
• isRec : Bool
• isUnsafe : Bool
• isReflexive : Bool
• lparams : List Level
• params : Array Expr
• compFields : Array Name
• compFieldVars : Array Expr
• indices : Array Expr
• val : Expr

@[reducible, inline]

abbrev Lean.Elab.ComputedFields.M (α : Type) : Type

Equations

• Lean.Elab.ComputedFields.M = ReaderT Lean.Elab.ComputedFields.Context Lean.MetaM

def Lean.Elab.ComputedFields.getComputedFieldValue (computedField : Name) (ctorTerm : Expr) : MetaM Expr

Equations

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

def Lean.Elab.ComputedFields.validateComputedFields : M Unit

Equations

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

def Lean.Elab.ComputedFields.mkImplType : M Unit

Equations

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

def Lean.Elab.ComputedFields.overrideCasesOn : M Unit

Equations

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

def Lean.Elab.ComputedFields.overrideConstructors : M Unit

Equations

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

def Lean.Elab.ComputedFields.overrideComputedFields : M Unit

Equations

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

def Lean.Elab.ComputedFields.mkComputedFieldOverrides (declName : Name) (compFields : Array Name) : MetaM Unit

Equations

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

def Lean.Elab.ComputedFields.setComputedFields (computedFields : Array (Name × Array Name)) : MetaM Unit

Sets the computed fields for a block of mutual inductives, adding the implementation via implemented_by.

The computedFields argument contains a pair for every inductive in the mutual block, consisting of the name of the inductive and the names of the associated computed fields.

Equations

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