Agda中列表字面量（尤其是多元素）的推荐编写语法

目前Agda标准库中，不同长度列表的标准合法写法如下：

open import Data.Nat
open import Data.List

zeroElements oneElement multipleElements : List ℕ
zeroElements = []
oneElement = [ 0 ]
multipleElements = 0 ∷ 1 ∷ 2 ∷ []

关键语法说明 #

• 空列表直接使用[]表示
• 单元素列表可使用方括号写法[ x ]，注意方括号和内部元素之间必须保留空格，写为[x]会触发解析错误
• 列表构造符∷是Unicode编码为U+2237的字符，并非ASCII编码的双冒号::
• 方括号+逗号分隔的多元素写法（例如[ 0 , 1 , 2 ]）不是Agda内置支持的标准语法，默认环境下无法通过编译。

根据Agda标准库的相关公开讨论结论：截至当前最新稳定版本，Agda暂未提供官方的更简洁多元素列表字面量语法，社区通用的首选写法就是使用∷依次拼接元素、末尾以空列表[]结尾的形式。
个人本地项目中可以通过自定义语法宏实现逗号分隔的方括号列表写法，但这类自定义语法不属于标准规范，不具备跨项目兼容性，不推荐在公共协作项目中使用。

内容的提问来源于stack exchange，提问作者Jo Liss