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

• eagerly realizing the equations when they are set to a non-default value
• when realizing them lazily, reset the options to their default

Equations

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

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

instance Lean.Meta.instInhabitedEqnsExtState : Inhabited EqnsExtState

Equations

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

def Lean.Meta.instInhabitedEqnsExtState.default : EqnsExtState

Equations

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

opaque Lean.Meta.eqnsExt : EnvExtension EqnsExtState

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

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

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

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

If any equation theorem affecting option is not the default value, create the equations now.

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.