michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

improved intro to cong4

Browse source
This commit is contained in:
wadler 2020-07-08 11:50:04 +01:00
parent 36ef980840
commit 78da4246b6
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/part2/Properties.lagda.md
View file

@ -1383,9 +1383,9 @@ Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` abo
When we introduced reduction, we claimed it was deterministic.
For completeness, we present a formal proof here.
A case term takes four arguments (three subterms and a bound
variable), and our proof will need a variant
of congruence to deal with functions of four arguments. It
Our proof will need a variant
of congruence to deal with functions of four arguments
(to deal with `case_[zero⇒_|suc_⇒_]`). It
is exactly analogous to `cong` and `cong₂` as defined previously:
```
cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E)