From 6feff8bd5efd31fe0488c61b39c53c6df9916a5e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 21 Oct 2024 21:19:35 +1100 Subject: [PATCH] fix test --- test/array.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/array.lean b/test/array.lean index 2ba3a29577..89f784293e 100644 --- a/test/array.lean +++ b/test/array.lean @@ -10,7 +10,7 @@ variable (g : i < (a.set! i v).size) variable (j_lt : j < (a.set! i v).size) #check_simp (a.set! i v).get ⟨i, g⟩ ~> v -#check_simp (a.set! i v).get! i ~> if i < a.size then v else default +#check_simp (a.set! i v).get! i ~> (a.setD i v)[i]! #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d #check_simp (a.set! i v)[i] ~> v