From 77499be10cdc4b26d45f2ee1d4d17e2a3a385b53 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 21 Apr 2020 15:42:33 -0300 Subject: [PATCH] Modified Peter's proposed text on argument order --- src/plfa/part2/Properties.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index c45d0a84..57f4178c 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -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 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` clauses in the definition of `_[_:=_]` need to be simplified, and the `with` clauses in `subst` need to match these exactly. The guideline is