Update Lambda.lagda.md Diamond and confluence example #1071
Conversation
There was a problem hiding this comment.
Your fix is incorrect. Please submit the following fix instead. Replace
"If each line stands for zero or more reduction steps, this is called confluence, while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property."
-->
"If each line in the figure above stands for zero or more reduction steps, this is called confluence, while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property."
|
OK, I saw each direction as a combination of 3 lines, as the individual characters. |
|
I have updated the change. What do you think about making it clear that the individual characters |
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.
Make description of picture clearer
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.