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

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.

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.

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 == Lean.Name.mkStr1 "_discr")

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 == Lean.Name.mkStr1 "_fun_discr")