part1/Decidable: Renaming proof (#496)

2020-07-25 01:48:25 +08:00 · 2020-07-25 01:48:25 +08:00 · 4e40ef4ab3
commit 4e40ef4ab3
parent 4e287a06f1
1 changed files with 1 additions and 1 deletions
--- a/src/plfa/part1/Decidable.lagda.md
+++ b/src/plfa/part1/Decidable.lagda.md
@ -573,7 +573,7 @@ from `m` only if `n ≤ m`:
 ```
 minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
 minus m       zero    _         = m
-minus (suc m) (suc n) (s≤s m≤n) = minus m n m≤n
+minus (suc m) (suc n) (s≤s n≤m) = minus m n n≤m
 ```

 Unfortunately, it is painful to use, since we have to explicitly provide