Skip to content

Commit bea2001

Browse files
committed
Update Lambda.lagda.md Diamond and confluence example
The diamond property written in Agda demand a single step from L->(M|N)? Therefore the verbose text should reflect the picture, which has 3 lines at the top.
1 parent ce50e93 commit bea2001

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/plfa/part2/Lambda.lagda.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -793,8 +793,8 @@ It can be illustrated as follows:
793793
Here `L`, `M`, `N` are universally quantified while `P`
794794
is existentially quantified. If each line stands for zero
795795
or more reduction steps, this is called confluence,
796-
while if the top two lines stand for a single reduction
797-
step and the bottom two stand for zero or more reduction
796+
while if the top three lines stand for a single reduction
797+
step and the bottom three stand for zero or more reduction
798798
steps it is called the diamond property. In symbols:
799799

800800
```agda

0 commit comments

Comments
 (0)