# 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`.

source
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

source
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]

Instances For

source
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)

Instances For

source
structure Lean.Elab.ComputedFields.Context extends 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

Instances For

source
@[reducible, inline]
abbrev Lean.Elab.ComputedFields.M (α : Type) :
Type
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For