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

CHANGELOG.md

@@ -147,6 +147,9 @@ 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 `pure` instead.
+
 * 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/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 ∷ []
+pure : A → List A
+pure = [_]
 
 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; []; _∷_; _++_; 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 = List.pure
   ; _<*>_  = ap
   }
 

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Bool.ListAction using (any)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List hiding (find; and; or; all; any)
+open import Data.List.Base as List hiding (find; and; or; all; any; pure)
 open import Data.List.Effectful as List using (monad)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional

src/IO.agda

@@ -63,7 +63,7 @@ module Colist where
 
 module List where
 
-  open import Data.List.Base
+  open import Data.List.Base hiding (pure)
 
   sequence : List (IO A) → IO (List A)
   sequence []       = ⦇ [] ⦈

src/Text/Format/Generic.agda

@@ -11,7 +11,7 @@ module Text.Format.Generic where
 open import Level using (0ℓ)
 open import Effect.Applicative
 open import Data.Char.Base using (Char)
-open import Data.List.Base as List hiding (sum)
+open import Data.List.Base as List hiding (sum; pure)
 open import Data.Maybe.Base as Maybe
 open import Data.Nat.Base
 open import Data.Nat.ListAction using (sum)