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 : Lean.TagAttribute

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

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

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

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

@[inline, reducible]

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

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

def Lean.Elab.ComputedFields.validateComputedFields : Lean.Elab.ComputedFields.M Unit

def Lean.Elab.ComputedFields.mkImplType : Lean.Elab.ComputedFields.M Unit

def Lean.Elab.ComputedFields.overrideCasesOn : Lean.Elab.ComputedFields.M Unit

def Lean.Elab.ComputedFields.overrideConstructors : Lean.Elab.ComputedFields.M Unit

def Lean.Elab.ComputedFields.overrideComputedFields : Lean.Elab.ComputedFields.M Unit

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

def Lean.Elab.ComputedFields.setComputedFields (computedFields : Array (Lake.Name × Array Lake.Name)) : Lean.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.