Modified Peter's proposed text on argument order

This commit is contained in:
Philip Wadler 2020-04-21 15:42:33 -03:00 committed by GitHub
parent 8da824a96a
commit 77499be10c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -775,7 +775,7 @@ Where the construct introduces a bound variable we need to compare it
with the substituted variable, applying the drop lemma if they are with the substituted variable, applying the drop lemma if they are
equal and the swap lemma if they are distinct. equal and the swap lemma if they are distinct.
Note that for Agda it makes a difference whether we write `x ≟ y` or For Agda it makes a difference whether we write `x ≟ y` or
`y ≟ x`. In an interactive proof, Agda will show which residual `with` `y ≟ x`. In an interactive proof, Agda will show which residual `with`
clauses in the definition of `_[_:=_]` need to be simplified, and the clauses in the definition of `_[_:=_]` need to be simplified, and the
`with` clauses in `subst` need to match these exactly. The guideline is `with` clauses in `subst` need to match these exactly. The guideline is