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
- name : Lake.Name
- type : Lean.Expr
- numParams : Nat
- numIndices : Nat
- isRec : Bool
- isUnsafe : Bool
- isReflexive : Bool
- isNested : Bool
- val : Lean.Expr
Sets the computed fields for a block of mutual inductives,
adding the implementation via
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.
- One or more equations did not get rendered due to their size.