From cb18af61846bd2c36b2f37e53302b4068f5e7cfa Mon Sep 17 00:00:00 2001
From: Daniel Fabian <daniel.fabian@integral-it.ch>
Date: Fri, 16 Apr 2021 11:14:36 +0000
Subject: [PATCH] feat: add `withLocalDecls` and `withLocalDeclsD`

They are array versions of `withLocalDecl` and `withLocalDeclD`, respectively. They are useful when you need to create variables dynamically.
---
 src/Lean/Meta/Basic.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index dee91fae30..3be257eaeb 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -883,6 +883,29 @@ def withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n
 def withLocalDeclD (name : Name) (type : Expr) (k : Expr → n α) : n α :=
   withLocalDecl name BinderInfo.default type k
 
+partial def withLocalDecls 
+    [Inhabited α]
+    (declInfos : Array (Name × BinderInfo × (Array Expr → n Expr)))
+    (k : (xs : Array Expr) → n α)
+    : n α := 
+  let rec loop 
+      [Inhabited α]
+      (acc : Array Expr) : n α := do
+    if acc.size < declInfos.size then
+      let (name, bi, typeCtor) := declInfos[acc.size]
+      withLocalDecl name bi (←typeCtor acc) fun x => loop (acc.push x) 
+    else k acc 
+          
+  loop #[] 
+
+def withLocalDeclsD
+    [Inhabited α]
+    (declInfos : Array (Name × (Array Expr → n Expr)))
+    (k : (xs : Array Expr) → n α)
+    : n α := 
+  withLocalDecls 
+    (declInfos.map (fun (name, typeCtor) => (name, BinderInfo.default, typeCtor))) k
+
 private def withLetDeclImp (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α := do
   let fvarId ← mkFreshId
   let ctx ← read