fix test

leanprover-community · Oct 21, 2024 · 6feff8b · 6feff8b
1 parent 78dfbc7
commit 6feff8b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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