partial def
Lean.Meta.GeneralizeTelescope.updateTypes
(e : Lean.Expr)
(eNew : Lean.Expr)
(entries : Array Lean.Meta.GeneralizeTelescope.Entry)
(i : Nat)
:
partial def
Lean.Meta.GeneralizeTelescope.generalizeTelescopeAux
{α : Type}
(k : Array Lean.Expr → Lean.MetaM α)
(entries : Array Lean.Meta.GeneralizeTelescope.Entry)
(i : Nat)
(fvars : Array Lean.Expr)
:
def
Lean.Meta.generalizeTelescope
{α : Type}
(es : Array Lean.Expr)
(k : Array Lean.Expr → Lean.MetaM α)
:
Equations
- Lean.Meta.generalizeTelescope es k = do let es ← Array.mapM (fun e => do let type ← Lean.Meta.inferType e let type ← Lean.Meta.instantiateMVars type pure { expr := e, type := type, modified := false }) es Lean.Meta.GeneralizeTelescope.generalizeTelescopeAux k es 0 #[]