From 568b598729662cd719a4a2ea7145348247d4e146 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2019 05:50:53 -0700 Subject: [PATCH] fix(library/init/data/array/basic): incorrect borrow annotation --- library/init/data/array/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 71bea32a76..14e8386135 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -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. -/