michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Make sum type right-associative

Browse source
This commit is contained in:
Georgi Lyubenov 2019-12-02 09:49:49 +02:00
parent 32a626789b
commit ef7f95b1db
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/extra/Logic.lagda
View file

@ -301,7 +301,7 @@ evidence that a disjunction holds.
We set the precedence of disjunction so that it binds less tightly We set the precedence of disjunction so that it binds less tightly
than any other declared operator. than any other declared operator.
\begin{code} \begin{code}
infix 1 _⊎_ infixr 1 _⊎_
\end{code} \end{code}
Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`. Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.

2
src/plfa/part1/Connectives.lagda.md
View file

@ -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 We set the precedence of disjunction so that it binds less tightly
than any other declared operator: than any other declared operator:
``` ```
infix 1 _⊎_ infixr 1 _⊎_
``` ```
Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`. Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.