Agda: std-lib: List: pattern matching with snoc

Question

I wrote a function to get everything but the last element of a List from std-lib:

open import Data.List

allButLast : ∀ {a} {A : Set a} → List A → List A
allButLast []       = []
allButLast (x ∷ []) = []
allButLast (x ∷ xs) = x ∷ allButLast xs

For proof purposes, I would like to rewrite this function using ∷ʳ instead:

allButLast2 : ∀ {a} {A : Set a} → List A → List A
allButLast2 []        = []
allButLast2 (xs ∷ʳ x) = xs

but I'm getting this error:

Could not parse the left-hand side allButLast2 (xs ∷ʳ x)
Operators used in the grammar:
  v.∷ʳ   (infixl operator, level 5) [_∷ʳ_ (/Users/fss/Dropbox/Documents/projects/Coding/dev/agda/agda-stdlib-1.4/src/Data/Vec/Base.agda:275,1-5)] 
  ∷ʳ (infixl operator, level 6) [_∷ʳ_ (/Users/fss/Dropbox/Documents/projects/Coding/dev/agda/agda-stdlib-1.4/src/Data/List/Base.agda:351,1-5)]
when scope checking the left-hand side allButLast2 (xs ∷ʳ x) in
the definition of allButLast2

I don't understand why it can't parse the left hand side of

allButLast2 (xs ∷ʳ x) = xs

Cactus Cactus · Accepted Answer · 2020-11-30T02:48:39

The _∷ʳ_ operator is a function, not a constructor or a pattern synonym, so it can't be used in a pattern:

infixl 6 _∷ʳ_

_∷ʳ_ : List A → A → List A
xs ∷ʳ x = xs ++ [ x ]

Agda: std-lib: List: pattern matching with snoc

1 Answers