[ refactor ] make Data.List.Base.[_] a pattern synonym

CHANGELOG.md

@@ -147,6 +147,11 @@ Non-backwards compatible changes
   their definitions and signatures updated to use `IsMagmaHomomorphism` and
   `IsMonoidHomomorphism` respectively
 
+* In `Data.List.Base`: the function definition `[_]` has been turned into
+  a `pattern` synonym, with a companion function definition `singleton` instead.
+  Similarly for `Data.List.NonEmpty.Base`, `Data.List.Fresh.NonEmpty`, and also
+  `Data.DifferenceList.Base`, where the notation `[_]` is introduced as `syntax`.
+
 * In `Data.List.DifferenceList.Base`: `take` and `drop` are deprecated
   because they do not have a lawful relationship to their `Data.List`
   counterparts. Consider using `viaList` if you want a lawful lifting

src/Data/DifferenceList/Base.agda

@@ -34,8 +34,11 @@ infixr 5 _∷_ _++_
 [] : DiffList A
 [] = id
 
-[_] : A → DiffList A
-[ x ] = x List.∷_
+singleton : A → DiffList A
+singleton = List._∷_
+
+singleton-syntax = singleton
+syntax singleton-syntax x = [ x ]
 
 _++_ : DiffList A → DiffList A → DiffList A
 _++_ = _∘′_

src/Data/DifferenceList/Properties.agda

@@ -9,7 +9,7 @@
 module Data.DifferenceList.Properties where
 
 open import Data.DifferenceList.Base
-  using (DiffList; fromList; toList; viaList; []; _∷_; [_]; _++_; _∷ʳ_; map)
+  using (DiffList; fromList; toList; viaList; []; _∷_; singleton-syntax; _++_; _∷ʳ_; map)
 open import Data.List.Base as List using (List)
 open import Data.List.Properties using (++-assoc; ++-identityʳ)
 open import Data.Product.Base using (Σ; _,_)

src/Data/List/Base.agda

@@ -42,6 +42,8 @@ private
 open import Agda.Builtin.List public
   using (List; []; _∷_)
 
+pattern [_] x = x ∷ []
+
 ------------------------------------------------------------------------
 -- Operations for transforming lists
 
@@ -156,8 +158,8 @@ length = foldr (const suc) 0
 ------------------------------------------------------------------------
 -- Operations for constructing lists
 
-[_] : A → List A
-[ x ] = x ∷ []
+singleton : A → List A
+singleton = [_]
 
 fromMaybe : Maybe A → List A
 fromMaybe (just x) = [ x ]

src/Data/List/Effectful.agda

@@ -9,8 +9,8 @@
 module Data.List.Effectful where
 
 open import Data.Bool.Base using (false; true)
-open import Data.List.Base
-  using (List; map; [_]; ap; []; _∷_; _++_; concat; concatMap)
+open import Data.List.Base as List
+  using (List; map; ap; []; _∷_; singleton; _++_; concat; concatMap)
 open import Data.List.Properties
   using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap
         ; concatMap-pure)
@@ -43,7 +43,7 @@ functor = record { _<$>_ = map }
 applicative : RawApplicative {ℓ} List
 applicative = record
   { rawFunctor = functor
-  ; pure = [_]
+  ; pure = singleton
   ; _<*>_  = ap
   }
 

src/Data/List/Fresh/NonEmpty.agda

@@ -33,6 +33,8 @@ record List#⁺ (A : Set a) (R : Rel A r) : Set (a ⊔ r) where
     tail : List# A R
     {rel} : fresh A R head tail
 
+pattern [_] x = x ∷#⁺ []
+
 open List#⁺
 
 ------------------------------------------------------------------------
@@ -41,8 +43,8 @@ open List#⁺
 uncons : List#⁺ A R → A × List# A R
 uncons (x ∷#⁺ xs) = x , xs
 
-[_] : A → List#⁺ A R
-[ x ] = x ∷#⁺ []
+singleton : A → List#⁺ A R
+singleton = [_]
 
 length : List#⁺ A R → ℕ
 length (x ∷#⁺ xs) = suc (List#.length xs)

src/Data/List/NonEmpty/Base.agda

@@ -40,6 +40,8 @@ record List⁺ (A : Set a) : Set a where
     head : A
     tail : List A
 
+pattern [_] x = x ∷ []
+
 open List⁺ public
 
 ------------------------------------------------------------------------
@@ -48,8 +50,8 @@ open List⁺ public
 uncons : List⁺ A → A × List A
 uncons (hd ∷ tl) = hd , tl
 
-[_] : A → List⁺ A
-[ x ] = x ∷ []
+singleton : A → List⁺ A
+singleton = [_]
 
 infixr 5 _∷⁺_
 

src/Data/Tree/Binary.agda

@@ -10,7 +10,8 @@ module Data.Tree.Binary where
 
 open import Level using (Level; _⊔_)
 open import Data.List.Base using (List)
-open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _∷ʳ_; _++_; [_])
+open import Data.DifferenceList as DiffList
+  using (DiffList; []; _∷_; _∷ʳ_; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Function.Base
 
@@ -80,7 +81,7 @@ module Suffix where
 module Leaves where
 
   toDiffList : Tree N L → DiffList L
-  toDiffList (leaf x)     = [ x ]
+  toDiffList (leaf x)     = DiffList.[ x ]
   toDiffList (node l m r) = toDiffList l ++ toDiffList r
 
   toList : Tree N L → List L

src/Data/Vec/Base.agda

@@ -37,6 +37,8 @@ data Vec (A : Set a) : ℕ → Set a where
   []  : Vec A zero
   _∷_ : ∀ (x : A) (xs : Vec A n) → Vec A (suc n)
 
+pattern [_] x = x ∷ []
+
 infix 4 _[_]=_
 
 data _[_]=_ {A : Set a} : Vec A n → Fin n → A → Set a where
@@ -240,8 +242,8 @@ countᵇ p = count (T? ∘ p)
 ------------------------------------------------------------------------
 -- Operations for building vectors
 
-[_] : A → Vec A 1
-[ x ] = x ∷ []
+singleton : A → Vec A 1
+singleton = [_]
 
 replicate : (n : ℕ) → A → Vec A n
 replicate zero    x = []

src/IO.agda

@@ -35,6 +35,7 @@ open import IO.Handle public
 module Colist where
 
   open import Codata.Musical.Colist.Base
+    using (Colist; []; _∷_; map)
 
   sequence : Colist (IO A) → IO (Colist A)
   sequence []       = pure []
@@ -64,6 +65,7 @@ module Colist where
 module List where
 
   open import Data.List.Base
+    using (List; []; _∷_; map)
 
   sequence : List (IO A) → IO (List A)
   sequence []       = ⦇ [] ⦈