3 
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 _∨_

示例代码中有部分代码。我只是想知道中缀器的含义是什么，以及为什么在那里使用它。

谢谢

4

1 回答 1

0
于 2013-06-30T13:13:37.097 回答