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

Lean.Meta.forallTelescopeCompatibleAux k 0 x x x = k x x x
Lean.Meta.forallTelescopeCompatibleAux k (Nat.succ i) x x x = do let type₁ ← Lean.Meta.whnf x let type₂ ← Lean.Meta.whnf x match type₁, type₂ with | Lean.Expr.forallE n₁ d₁ b₁ c₁, Lean.Expr.forallE n₂ d₂ b₂ c₂ => let _do_jp := fun y => do let a ← Lean.Meta.isDefEq d₁ d₂ let _do_jp : PUnit → Lean.MetaM α := fun y => let _do_jp := fun y => Lean.Meta.withLocalDecl n₁ (Lean.Expr.Data.binderInfo c₁) d₁ fun x => let type₁ := Lean.Expr.instantiate1 b₁ x; let type₂ := Lean.Expr.instantiate1 b₂ x; Lean.Meta.forallTelescopeCompatibleAux k i type₁ type₂ (Array.push x x); if (Lean.Expr.Data.binderInfo c₁ == Lean.Expr.Data.binderInfo c₂) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "binder annotation mismatch at parameter '" ++ Lean.toMessageData n₁ ++ Lean.toMessageData "'") _do_jp y if a = true then do let y ← pure PUnit.unit _do_jp y else do let a ← Lean.Meta.mkHasTypeButIsExpectedMsg d₁ d₂ let y ← Lean.throwError (Lean.toMessageData "parameter '" ++ Lean.toMessageData n₁ ++ Lean.toMessageData "' " ++ Lean.toMessageData a ++ Lean.toMessageData "") _do_jp y; if (n₁ == n₂) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "parameter name mismatch '" ++ Lean.toMessageData n₁ ++ Lean.toMessageData "', expected '" ++ Lean.toMessageData n₂ ++ Lean.toMessageData "'") _do_jp y | x, x_1 => Lean.throwError (Lean.toMessageData "unexpected number of parameters")

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 α

Equations

Lean.Meta.forallTelescopeCompatible type₁ type₂ numParams k = controlAt Lean.MetaM fun runInBase => Lean.Meta.forallTelescopeCompatibleAux (fun xs type₁ type₂ => runInBase (k xs type₁ type₂)) numParams type₁ type₂ #[]

source

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

Lean.Syntax × Option Lean.Syntax

Equations

Lean.Elab.expandOptDeclSig stx = let binders := Lean.Syntax.getOp stx 0; let optType := Lean.Syntax.getOp stx 1; if Lean.Syntax.isNone optType = true then (binders, none) else let typeSpec := Lean.Syntax.getOp optType 0; (binders, some (Lean.Syntax.getOp typeSpec 1))

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 x s x_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)

Equations

Lean.Elab.sortDeclLevelParams scopeParams allUserParams usedParams = match List.find? (fun u => !Array.contains usedParams u && !List.elem u scopeParams) allUserParams with | some u => throw (toString "unused universe parameter '" ++ toString u ++ toString "'") | none => let result := List.foldl (fun result levelName => if Array.elem levelName usedParams = true then levelName :: result else result) [] allUserParams; let remaining := Array.filter (fun levelParam => !List.elem levelParam allUserParams) usedParams 0 (Array.size usedParams); let remaining := Array.qsort remaining Lean.Name.lt 0 (Array.size remaining - 1); pure (result ++ Array.toList remaining)