Update Lambda.lagda.md Diamond and confluence example - #1071
Conversation
Sorry, something went wrong.
wadler
left a comment
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."
Sorry, something went wrong.
|
OK, I saw each direction as a combination of 3 lines, as the individual characters. |
Sorry, something went wrong.
|
I have updated the change. What do you think about making it clear that the individual characters \, / connect to a single line and the figure has 4 lines total? |
Sorry, something went wrong.
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
Reviewers
Requested changes must be addressed to merge this pull request.
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.