Agda: std-lib: 列表：与 snoc 的模式匹配

Question

我编写了一个函数来从 std-lib 中获取 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 ]

Agda: std-lib: 列表：与 snoc 的模式匹配

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

agda

agda-stdlib