max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add instantiateLevelParamsArray

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-01 12:16:34 -08:00
parent 427df087e8
commit 7dafba2c6c
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Lean/Expr.lean
View file

@ -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