列表文字的语法

发布于 2025-02-05 06:52:38 字数 565 浏览 1 评论 0原文

在AGDA中，写列表文字的首选方法是什么，尤其是使用多个元素？

我能想到的最好的是：（

open import Data.Nat
open import Data.List

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

请注意，[0]需要方括号内的空格。还请注意，>是Unicode U+2237，而不是ASCII Double Double 。

我希望Square Bracket语法能够使用多个元素，例如[0，1，2]，但情况似乎并非如此我是在阅读问题＃235 正确地说，不再有简洁的语法现在？

原文

In Agda, what's the preferred way to write list literals, especially with multiple elements?

The best I could come up with is:

open import Data.Nat
open import Data.List

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

(Note that [ 0 ] needs spaces inside the square brackets. Also note that ∷ is Unicode U+2237, not an ASCII double colon.)

I was hoping that the square bracket syntax would work with multiple elements, like [ 0 , 1 , 2 ], but this doesn't seem to be the case. Am I reading issue #235 correctly that there is no more concise syntax for this right now?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

羅雙樹 2025-02-12 06:52:38

这就是我在注意到您链接到一个问题之前想到的
在错误跟踪器上，一旦我们获得键入模式同义词，当时的现状并没有改善

module ListLiteral where

open import Agda.Builtin.List

infix 10 [_
infixr 15 _,_
infix 20 _]
pattern [_ x = x
pattern _,_ x xs = x ∷ xs
pattern _] x = x ∷ []

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

test : [ 1 , 2 , 3 , 4 ] ≡ _
test = refl

open import Agda.Builtin.Bool

isSingleton : List Nat → Bool
isSingleton ([ _ ]) = true
isSingleton _ = false

（NB：他们没有积极的努力来进行
实施它们）至少应该解决模式_，_的问题
与Sigma类型的构造函数冲突。

在我自己的项目中，我倾向于写a∷b∷c∷...。

This is what I came up with before noticing you were linking to an issue
on the bug tracker and it's no improvement over the status quo at the time

module ListLiteral where

open import Agda.Builtin.List

infix 10 [_
infixr 15 _,_
infix 20 _]
pattern [_ x = x
pattern _,_ x xs = x ∷ xs
pattern _] x = x ∷ []

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

test : [ 1 , 2 , 3 , 4 ] ≡ _
test = refl

open import Agda.Builtin.Bool

isSingleton : List Nat → Bool
isSingleton ([ _ ]) = true
isSingleton _ = false

Once we get typed pattern synonyms (NB: they are no active efforts to
implement them) it should at least solve the issue that the pattern _,_
clashes with the constructor for sigma types.

In my own projects I tend to just write a ∷ b ∷ c ∷ ....

回复收藏 0 原文

~没有更多了~