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

fix(library/init/data/array/basic): incorrect borrow annotation

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-03 05:50:53 -07:00
parent 19856c4ca7
commit 568b598729
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/array/basic.lean
View file

@ -87,7 +87,7 @@ def update (a : Array α) (i : @& Fin a.sz) (v : α) : Array α :=
`Fin` values are represented as tag pointers in the Lean runtime. Thus,
`update` may be slightly slower than `updt`. -/
@[extern cpp inline "lean::array_updt(#2, #3, #4)"]
def updt (a : @& Array α) (i : USize) (v : @& α) (h : i.toNat < a.sz) : Array α :=
def updt (a : Array α) (i : USize) (v : α) (h : i.toNat < a.sz) : Array α :=
a.update ⟨i.toNat, h⟩ v
/- "Comfortable" version of `update`. It performs a bound check at runtime. -/