Lean.Elab.AuxDiscr

def Lean.mkAuxDiscr {m : Type → Type} [inst : Monad m] [inst : Lean.MonadQuotation m] :

Create an auxiliary identifier for storing non-atomic discriminants. This kind of free variable is cleared before elaborating a match alternative rhs.

Equations

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

source

def Lean.mkAuxFunDiscr {m : Type → Type} [inst : Monad m] [inst : Lean.MonadQuotation m] :

m Lean.Ident

Create an auxiliary identifier for expanding notation such as fun (a, b) => .... This kind of free variable is cleared before elaborating a match alternative rhs.

Equations

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

source

def Lean.isAuxDiscrName (n : Lean.Name) :

Bool

Return true iff n is an auxiliary variable created by expandNonAtomicDiscrs?

Equations

Lean.isAuxDiscrName n = (Lean.Name.hasMacroScopes n && Lean.Name.eraseMacroScopes n == `_discr)

source

def Lean.isAuxFunDiscrName (n : Lean.Name) :

Bool

Return true iff n is an auxiliary variable created by notation such as fun (a, b) => .... They are cleared before eliminating the match alternatives RHS

Equations

Lean.isAuxFunDiscrName n = (Lean.Name.hasMacroScopes n && Lean.Name.eraseMacroScopes n == `_fun_discr)