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

Marks a function as a computed field of an inductive.

Computed fields are specified in the with-block of an inductive type declaration. They can be used to allow certain values to be computed only once at the time of construction and then later be accessed immediately.

Example:

inductive NatList where
  | nil
  | cons : Nat → NatList → NatList
with
  @[computed_field] sum : NatList → Nat
  | .nil => 0
  | .cons x l => x + l.sum
  @[computed_field] length : NatList → Nat
  | .nil => 0
  | .cons _ l => l.length + 1

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.