Lean.Elab.DeclUtil

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

Nat → Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM α

Equations

One or more equations did not get rendered due to their size.
Lean.Meta.forallTelescopeCompatibleAux k 0 _fun_discr _fun_discr _fun_discr = k _fun_discr _fun_discr _fun_discr

def Lean.Meta.forallTelescopeCompatible {α : Type} {m : Type → Type u_1} [inst : Monad m] [inst : MonadControlT Lean.MetaM m] (type₁ : Lean.Expr) (type₂ : Lean.Expr) (numParams : Nat) (k : Array Lean.Expr → Lean.Expr → Lean.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.

source

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

Lean.Syntax × Option Lean.Syntax

Equations

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

source

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

Lean.Syntax × Lean.Syntax

Equations

Lean.Elab.expandDeclSig stx = let binders := Lean.Syntax.getOp stx 0; let typeSpec := Lean.Syntax.getOp stx 1; (binders, Lean.Syntax.getOp typeSpec 1)

source

def Lean.Elab.mkFreshInstanceName (env : Lean.Environment) (nextIdx : Nat) :

Lean.Name

Equations

Lean.Elab.mkFreshInstanceName env nextIdx = Lean.Name.appendIndexAfter (Lean.Environment.mainModule env ++ `_instance) nextIdx

source

def Lean.Elab.isFreshInstanceName (name : Lean.Name) :

Bool

Equations

Lean.Elab.isFreshInstanceName name = match name with | Lean.Name.str a s a_1 => String.isPrefixOf "_instance" s | x => false

source

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

Except String (List Lean.Name)

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.