是什麼infixr在阿格達意思？

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

有從樣本碼的碼的一部分。我只是想知道的infixr是什麼意思，爲什麼它在那裏使用。是什麼infixr在阿格達意思？

由於

來源

2013-06-30 IanIsAFK

它設置_V_是右結合（infixl是左）： '一_V_ b _V_ C' 然後 '一個_V_（B _V_ C）'。的「1」是優先與其他中綴運算符混合。 –

這顯著不寫在表達括號像

一個∧ b ∨Ç

一個* b +Ç

infixr/infixl - 是一個功率與（R =右，L =左），當它是我們ED中綴（之間）的位置

來源

2013-06-30 13:13:37 wit

是什麼infixr在阿格達意思？

回答

相關問題