what is the meaning of infixr in Agda?

Question

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

there is part of code from a sample code. I am just wondering what the meaning of the infixr, and why it be used there.

Thanks

Answer 1

This is significant not to write parentheses in expression like

a ∧ b ∨ c

a * b + c

infixr/infixl - is a power to (r=right, l=left), when it is used in infix(between) position