Agda: std: List:模式匹配

Question

我编写了一个函数来获取除了std中的List的最后一个元素之外的所有内容：

open import Data.List

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

为了证明起见，我想用∷ʳ重写这个函数：

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

但我发现了一个错误：

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

我不明白为什么它不能解析

allButLast2 (xs ∷ʳ x) = xs

Answer 1

The _∷ʳ_ operator is a function, not a constructor or a pattern synonym，因此不能在模式中使用：

infixl 6 _∷ʳ_

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