在Agda中，可以使用snoc函数来将一个元素添加到列表的末尾。为了得到除了最后一个元素之外的所有元素，可以使用递归的方式实现。下面是一个示例代码：

open import Data.List
open import Data.Nat

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

example : allButLast [1, 2, 3, 4] ≡ [1, 2, 3]
example = refl

在这个例子中，allButLast函数接受一个类型为List A的列表作为输入，并返回一个类型为List A的列表。首先，我们处理空列表的情况，直接返回空列表。然后，如果列表只有一个元素，同样返回空列表。最后，对于其他情况，我们递归地调用allButLast函数，并将列表的头部元素添加到结果列表中。

注意，在代码中我使用了refl来表示相等性证明。这是因为allButLast [1, 2, 3, 4]和[1, 2, 3]在类型上是相等的。如果你在Agda中运行这段代码，你会看到Agda会自动验证这个相等性。

希望这个示例能对你有所帮助！