From 7dafba2c6c20558ebb3a4fe5195a867478d0a8ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2019 12:16:34 -0800
Subject: [PATCH] feat: add `instantiateLevelParamsArray`

---
 src/Init/Lean/Expr.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index d4e9e38d85..70c875e7cc 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -830,5 +830,18 @@ private def getParamSubst : List Name → List Level → Name → Option Level
 def instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr :=
 instantiateLevelParamsCore (getParamSubst paramNames lvls) e
 
+private partial def getParamSubstArray (ps : Array Name) (us : Array Level) (p' : Name) : Nat → Option Level
+| i =>
+  if h : i < ps.size then
+    let p := ps.get ⟨i, h⟩;
+    if h : i < us.size then
+      let u := us.get ⟨i, h⟩;
+      if p == p' then some u else getParamSubstArray (i+1)
+    else none
+  else none
+
+def instantiateLevelParamsArray (e : Expr) (paramNames : Array Name) (lvls : Array Level) : Expr :=
+instantiateLevelParamsCore (fun p => getParamSubstArray paramNames lvls p 0) e
+
 end Expr
 end Lean