【发布时间】：2013-06-30 10:36:04
【问题描述】：
Prp : Set₁
Prp = Set
data _∧_ (P Q : Prp) : Prp where
∧-intro : P -> Q -> P ∧ Q
infixr 2 _∧_
data _∨_ (P Q : Prp) : Prp where
∨-intro₁ : P -> P ∨ Q
∨-intro₂ : Q -> P ∨ Q
infixr 1 _∨_
示例代码中有部分代码。我只是想知道中缀器的含义是什么，以及为什么在那里使用它。
谢谢
【问题讨论】：
-
它将 V 设置为右关联（中缀l在左）：'a V b V c ' 然后是 'a V (b V c)'。 '1' 是与其他中缀运算符混合时的优先级。
标签： agda