fix

leanprover · Jan 12, 2025 · cdcb578 · cdcb578
1 parent fa78cf7
commit cdcb578
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
@@ -1508,7 +1508,7 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
 
 /-! ### singleton -/
 
-@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
+@[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
 
 /-! ### append -/