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

Equations

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

def Lean.Elab.ComputedFields.isScalarField (ctor : Lake.Name) : Lean.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 : Lake.Name
• levelParams : List Lake.Name
• type : Lean.Expr
• numParams : Nat
• numIndices : Nat
• all : List Lake.Name
• ctors : List Lake.Name
• numNested : Nat
• isRec : Bool
• isUnsafe : Bool
• isReflexive : Bool
• lparams : List Lean.Level
• params : Array Lean.Expr
• compFields : Array Lake.Name
• compFieldVars : Array Lean.Expr
• indices : Array Lean.Expr
• val : Lean.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 : Lake.Name) (ctorTerm : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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