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

Instances For
    @[inline, reducible]
    Instances For

      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.

      Instances For