# Documentation

Lean.Elab.ComputedFields

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

Equations
Equations
• = do let __do_lift ← pure (__do_lift.numFields == 0)
• lparams :
• params :
• compFields :
• compFieldVars :
• indices :
• val : Lean.Expr
Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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.