From ef7f95b1db156f9026036b0adb955c6826829166 Mon Sep 17 00:00:00 2001
From: Georgi Lyubenov <godzbanebane@gmail.com>
Date: Mon, 2 Dec 2019 09:49:49 +0200
Subject: [PATCH] Make sum type right-associative

---
 extra/extra/Logic.lagda             | 2 +-
 src/plfa/part1/Connectives.lagda.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/extra/extra/Logic.lagda b/extra/extra/Logic.lagda
index aa86e676..0c4e0cfc 100644
--- a/extra/extra/Logic.lagda
+++ b/extra/extra/Logic.lagda
@@ -301,7 +301,7 @@ evidence that a disjunction holds.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator.
 \begin{code}
-infix 1 _⊎_
+infixr 1 _⊎_
 \end{code}
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 
diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md
index 9968c87b..e40c895d 100644
--- a/src/plfa/part1/Connectives.lagda.md
+++ b/src/plfa/part1/Connectives.lagda.md
@@ -389,7 +389,7 @@ simplify to the same term, and similarly for `inj₂ y`.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator:
 ```
-infix 1 _⊎_
+infixr 1 _⊎_
 ```
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.