Array spellings

Author: TwoFX

src/Init/Data/Array/Basic.lean

@@ -18,11 +18,15 @@ universe u v w
 
 /-! ### Array literal syntax -/
 
+/-- Syntax for `Array α`. -/
 syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
 
 macro_rules
   | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
 
+recommended_spelling "#[]" "empty" «term#[_,]»
+recommended_spelling "#[x]" "singleton" «term#[_,]»
+
 variable {α : Type u}
 
 namespace Array