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

Question

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

any ideal what is << >> mean?

or what the meaning of

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

thanks

score 5 · Accepted Answer

有三个参数，_∷⟪_⟫_其中下划线。

为方便起见，请在下面编号_1 ∷ ⟪ _2 ⟫ _3：

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

_1 : (x : ℕ)

_2 : min ≤ x

_3 : MinList x

<< 和 >> unicode 只是名称，没什么特别的。看

和

score 3 · Accepted Answer

Agda 允许定义任意数量的“运算符”（在这种情况下，它是一个类型构造函数）（也就是说，可以接受任意数量的参数），每个参数的位置用下划线表示，所以_∷⟪_⟫_可以写成三个参数的常规函数：

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

并称为（对于这两种情况）

x ::⟪ n ⟫ y

minCons x n y

2 回答 2