# Documentation

Lean.Elab.DeclUtil

Equations
• One or more equations did not get rendered due to their size.
• = k x x x
def Lean.Meta.forallTelescopeCompatible {α : Type} {m : TypeType u_1} [inst : ] [inst : ] (type₁ : Lean.Expr) (type₂ : Lean.Expr) (numParams : Nat) (k : Lean.ExprLean.Exprm α) :
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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• = let binders := stx[0]; let typeSpec := stx[1]; (binders, typeSpec[1])
Equations
def Lean.Elab.sortDeclLevelParams (scopeParams : ) (allUserParams : ) (usedParams : ) :

Sort the given list of usedParams using the following order:

• If it is an explicit level allUserParams, then use user given order.
• Otherwise, use lexicographical.

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: explicitParams 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.