opaque Lean.Meta.backward.eqns.nonrecursive : Lean.Option Bool

opaque Lean.Meta.backward.eqns.deepRecursiveSplit : Lean.Option Bool

def Lean.Meta.eqnAffectingOptions : Array (Lean.Option Bool)

These options affect the generation of equational theorems in a significant way. For these, their value at definition time, not realization time, should matter.

This is implemented by storing their values at definition time (when non-default) in an environment extension, and restoring them when the equations are lazily realized.

Equations

• Lean.Meta.eqnAffectingOptions = #[Lean.Meta.backward.eqns.nonrecursive, Lean.Meta.backward.eqns.deepRecursiveSplit, Lean.backward.defeqAttrib.useBackward]

opaque Lean.Meta.eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue))

Environment extension that stores the values of eqnAffectingOptions at definition time, keyed by declaration name. Only populated when at least one option has a non-default value. Stores an association list of (option name, value) pairs for options that differ from defaults.

def Lean.Meta.eqnThmSuffixBase : String

Equations

• Lean.Meta.eqnThmSuffixBase = "eq"

def Lean.Meta.eqnThmSuffixBasePrefix : String

Equations

• Lean.Meta.eqnThmSuffixBasePrefix = Lean.Meta.eqnThmSuffixBase ++ "_"

def Lean.Meta.eqn1ThmSuffix : String

Equations

• Lean.Meta.eqn1ThmSuffix = Lean.Meta.eqnThmSuffixBasePrefix ++ "1"

def Lean.Meta.isEqnReservedNameSuffix (s : String) : Bool

Returns true if s is of the form eq_<idx>

Equations

• Lean.Meta.isEqnReservedNameSuffix s = (Lean.Meta.eqnThmSuffixBasePrefix.isPrefixOf s && (s.drop 3).isNat)

def Lean.Meta.unfoldThmSuffix : String

Equations

• Lean.Meta.unfoldThmSuffix = "eq_def"

def Lean.Meta.eqUnfoldThmSuffix : String

Equations

• Lean.Meta.eqUnfoldThmSuffix = "eq_unfold"

def Lean.Meta.isEqnLikeSuffix (s : String) : Bool

Equations

• Lean.Meta.isEqnLikeSuffix s = (s == Lean.Meta.unfoldThmSuffix || s == Lean.Meta.eqUnfoldThmSuffix || Lean.Meta.isEqnReservedNameSuffix s)

def Lean.Meta.declFromEqLikeName (env : Environment) (name : Name) : Option (Name × String)

The equational theorem for a definition can be private even if the definition itself is not. So un-private the name here when looking for a declaration

Equations

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

def Lean.Meta.mkEqLikeNameFor (env : Environment) (declName : Name) (suffix : String) : Name

Equations

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

def Lean.Meta.ensureEqnReservedNamesAvailable (declName : Name) : CoreM Unit

Throw an error if names for equation theorems for declName are not available.

Equations

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

def Lean.Meta.GetEqnsFn : Type

Equations

• Lean.Meta.GetEqnsFn = (Lean.Name → Lean.MetaM (Option (Array Lean.Name)))

def Lean.Meta.registerGetEqnsFn (f : GetEqnsFn) : IO Unit

Registers a new function for retrieving equation theorems. We generate equations theorems on demand, and they are generated by more than one module. For example, the structural and well-founded recursion modules generate them. Most recent getters are tried first.

A getter returns an Option (Array Name). The result is none if the getter failed. Otherwise, it is a sequence of theorem names where each one of them corresponds to an alternative. Example: the definition

def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs

should have two equational theorems associated with it

f [] = []

and

(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs

Equations

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

structure Lean.Meta.EqnsExtState : Type

A mapping from equational theorem to the declaration it was derived from.

• mapInv : PHashMap Name Name

@[implicit_reducible]

instance Lean.Meta.instInhabitedEqnsExtState : Inhabited EqnsExtState

Equations

• Lean.Meta.instInhabitedEqnsExtState = { default := Lean.Meta.instInhabitedEqnsExtState.default }

opaque Lean.Meta.eqnsExt : EnvExtension EqnsExtState

A mapping from equational theorem to the declaration it was derived from.

def Lean.Meta.withEqnOptions {α : Type} (declName : Name) (act : MetaM α) : MetaM α

Runs act with the equation-affecting options restored to the values stored for declName at definition time (or reset to their defaults if none were stored). Use this inside realizeConst callbacks, which otherwise see the caller-independent ctx.opts rather than the outer getEqnsFor? context.

Equations

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

def Lean.Meta.mkSimpleEqThm (declName name : Name) : MetaM (Option Name)

Simple equation theorem for nonrecursive definitions.

Equations

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

def Lean.Meta.isEqnThm? (thmName : Name) : CoreM (Option Name)

Returns some declName if thmName is an equational theorem for declName.

Equations

• Lean.Meta.isEqnThm? thmName = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.Meta.eqnsExt.getState __do_lift).mapInv thmName)

def Lean.Meta.isEqnThm (thmName : Name) : CoreM Bool

Returns true if thmName is an equational theorem.

Equations

• Lean.Meta.isEqnThm thmName = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.contains (Lean.Meta.eqnsExt.getState __do_lift).mapInv thmName)

def Lean.Meta.getEqnsFor? (declName : Name) : MetaM (Option (Array Name))

Returns equation theorems for the given declaration.

Equations

• Lean.Meta.getEqnsFor? declName = Lean.Meta.withLCtx { } ∅ (Lean.Meta.withEqnOptions declName (Lean.Meta.getEqnsFor?Core✝ declName))

def Lean.Meta.saveEqnAffectingOptions (declName : Name) : MetaM Unit

If any equation theorem affecting option is not the default value, store the option values for later use during lazy equation generation.

Equations

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

def Lean.Meta.GetUnfoldEqnFn : Type

Equations

• Lean.Meta.GetUnfoldEqnFn = (Lean.Name → Lean.MetaM (Option Lean.Name))

def Lean.Meta.registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit

Registers a new function for retrieving a "unfold" equation theorem.

We generate this kind of equation theorem on demand, and it is generated by more than one module. For example, the structural and well-founded recursion modules generate it. Most recent getters are tried first.

A getter returns an Option Name. The result is none if the getter failed. Otherwise, it is a theorem name. Example: the definition

def f (xs : List Nat) : List Nat :=
  match xs with
  | [] => []
  | x::xs => (x+1)::f xs

should have the theorem

(xs : Nat) →
  f xs =
    match xs with
    | [] => []
    | x::xs => (x+1)::f xs

Equations

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

def Lean.Meta.getUnfoldEqnFor? (declName : Name) (nonRec : Bool := false) : MetaM (Option Name)

Returns an "unfold" theorem (f.eq_def) for the given declaration. By default, we do not create unfold theorems for nonrecursive definitions. You can use nonRec := true to override this behavior.

Equations

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