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

This file implements the computed fields feature by simulating it via implemented_by. The main function is setComputedFields.

Equations
    Instances For
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    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.

                      Equations
                        Instances For