_∷«_»_：（X：ℕ） - >分≤X - > MinList X - > MinList分钟

data MinList (min : ℕ) : Set where 
    [] : MinList min 
    _∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

或什么的

_∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

意义感谢

2013-06-30 IanIsAFK

有在_∷⟪_⟫_三个参数这是下划线。

编号他们_1 ∷ ⟪ _2 ⟫ _3下面方便：

类型(x : ℕ) -> min ≤ x -> MinList x -> MinList min有3个参数和结果类型。

_1 : (x : ℕ)

_2 : min ≤ x

_3 : MinList x

的< <和Unicode的>>都只是名字，没有什么特别的。见

和

2013-06-30 11:17:12

是不是误导叫'«'和'»'的名字，当他们在这里只是作为一个单一的名字'的部分_∷ «_»_'？ – Rotsor

迂腐，名字是'∷'''和'»'，其中第一个是两个unicode字符长，'∷'和'«'。 –

2007 Ulf Norell博士论文，第5.1.1小节。名称，第97页，称这些*名称部分*，并且“A *名称*是一个非空序列的交替名称部分和_”。 – Rotsor

阿格达允许定义“经营者”（在这种情况下，这是一个类型构造）的任意参数数量（即的，可以采取任意数量的参数），每个参数的位置用下划线表示，所以_∷⟪_⟫_可以写成三个参数的常规函数：

minCons : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

和称为（对于这两种情况下）

x ::⟪ n ⟫ y 

minCons x n y

2013-06-30 11:15:39 huon

回答