From 06bb3a82d341930b8748f68eafbb82189dc87ca5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Sep 2019 13:41:42 -0700
Subject: [PATCH] feat(library/init/lean/localcontext): add
 `LocalContext.mkLambda` and `LocalContext.mkForall`

---
 library/init/lean/localcontext.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean
index 46843b1fc9..097a5e93f8 100644
--- a/library/init/lean/localcontext.lean
+++ b/library/init/lean/localcontext.lean
@@ -234,5 +234,28 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) : Nat → N
 def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) : Bool :=
 isSubPrefixOfAux lctx₁.decls lctx₂.decls 0 0
 
+@[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
+let b := b.abstract xs;
+xs.size.foldRev (fun i b =>
+  let x := xs.get i;
+  match lctx.findFVar x with
+  | some (LocalDecl.cdecl _ _ n ty bi)  =>
+    let ty := ty.abstractRange i xs;
+    if isLambda then
+      Expr.lam n bi ty b
+    else
+      Expr.pi n bi ty b
+  | some (LocalDecl.ldecl _ _ n ty val) =>
+    let ty  := ty.abstractRange i xs;
+    let val := val.abstractRange i xs;
+    Expr.elet n ty val b
+  | none => b) b
+
+def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
+mkBinding true lctx xs b
+
+def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
+mkBinding false lctx xs b
+
 end LocalContext
 end Lean