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 :

Lean.TagAttribute

source

def Lean.Elab.ComputedFields.mkUnsafeCastTo (expectedType : Lean.Expr) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Elab.ComputedFields.mkUnsafeCastTo expectedType e = Lean.Meta.mkAppOptM `unsafeCast #[none, some expectedType, some e]

source

def Lean.Elab.ComputedFields.isScalarField (ctor : Lean.Name) :

Lean.CoreM Bool

Equations

Lean.Elab.ComputedFields.isScalarField ctor = do let __do_lift ← Lean.getConstInfoCtor ctor pure (__do_lift.numFields == 0)

source

structure Lean.Elab.ComputedFields.Contextextends Lean.InductiveVal :

Type

lparams : List Lean.Level
params : Array Lean.Expr
compFields : Array Lean.Name
compFieldVars : Array Lean.Expr
indices : Array Lean.Expr
val : Lean.Expr

Instances For

source

@[inline]

abbrev Lean.Elab.ComputedFields.M (α : Type) :

Type

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Elab.ComputedFields.validateComputedFields :

Lean.Elab.ComputedFields.M Unit

Equations

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

source

def Lean.Elab.ComputedFields.mkImplType :

Lean.Elab.ComputedFields.M Unit

Equations

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

source

def Lean.Elab.ComputedFields.overrideCasesOn :

Lean.Elab.ComputedFields.M Unit

Equations

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

source

def Lean.Elab.ComputedFields.overrideConstructors :

Lean.Elab.ComputedFields.M Unit

Equations

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

source

def Lean.Elab.ComputedFields.overrideComputedFields :

Lean.Elab.ComputedFields.M Unit

Equations

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

source

def Lean.Elab.ComputedFields.mkComputedFieldOverrides (declName : Lean.Name) (compFields : Array Lean.Name) :

Lean.MetaM Unit

Equations

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

source

def Lean.Elab.ComputedFields.setComputedFields (computedFields : Array (Lean.Name × Array Lean.Name)) :

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