def Lean.Meta.forallTelescopeCompatibleAux {α : Type} (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.forallTelescopeCompatibleAux k 0 x✝² x✝¹ x✝ = k x✝ x✝² x✝¹

def Lean.Meta.forallTelescopeCompatible {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] (type₁ type₂ : Expr) (numParams : Nat) (k : Array Expr → Expr → Expr → m α) : m α

Given two forall-expressions type₁ and type₂, ensure the first numParams parameters are compatible, and then execute k with the parameters and remaining types.

Equations

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

def Lean.Elab.expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax

Equations

• Lean.Elab.expandOptDeclSig stx = if stx[1].isNone = true then (stx[0], none) else let typeSpec := stx[1][0]; (stx[0], some typeSpec[1])

def Lean.Elab.expandDeclSig (stx : Syntax) : Syntax × Syntax

Equations

• Lean.Elab.expandDeclSig stx = (stx[0], stx[1][1])

def Lean.Elab.sortDeclLevelParams (scopeParams allUserParams : List Name) (usedParams : Array Name) : Except String (List Name)

Sort the given list of usedParams using the following order:

• If it is an explicit level in allUserParams, then use user-given order.
• All other levels come in lexicographic order after these.

Remark: scopeParams are the universe params introduced using the universe command. allUserParams contains the universe params introduced using the universe command and the .{...} notation.

Remark: this function return an exception if there is an u not in usedParams, that is in allUserParams but not in scopeParams.

Remark: scopeParams and allUserParams are in reverse declaration order. That is, the head is the last declared parameter.

Equations

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