From 11d829eccd8915ad718b2f37a55950093dffacc8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2019 10:20:52 -0800
Subject: [PATCH] feat: add `lambdaMetaTelescope`

We need it because `abstractMVars` use lambdas
---
 src/Init/Lean/Meta/Basic.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 5827e06166..737da62787 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -639,6 +639,31 @@ forallMetaTelescopeReducingAux false none #[] #[] 0 e
 def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
 forallMetaTelescopeReducingAux true maxMVars? #[] #[] 0 e
 
+/-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
+@[specialize] private partial def lambdaMetaTelescopeAux
+    (maxMVars? : Option Nat)
+    : Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
+| mvars, bis, j, Expr.lam n d b c => do
+  let d     := d.instantiateRevRange j mvars.size mvars;
+  mvar ← mkFreshExprMVar d;
+  let mvars := mvars.push mvar;
+  let bis   := bis.push c.binderInfo;
+  match maxMVars? with
+  | none          => lambdaMetaTelescopeAux mvars bis j b
+  | some maxMVars =>
+    if mvars.size < maxMVars then
+      lambdaMetaTelescopeAux mvars bis j b
+    else
+      let type := b.instantiateRevRange j mvars.size mvars;
+      pure (mvars, bis, type)
+| mvars, bis, j, type =>
+  let type := type.instantiateRevRange j mvars.size mvars;
+  pure (mvars, bis, type)
+
+/-- Similar to `forallMetaTelescope` but for lambda expressions. -/
+def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+lambdaMetaTelescopeAux maxMVars? #[] #[] 0 e
+
 @[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α :=
 fun _ s =>
   let (a, mctx) := x.run s.mctx;