Merge pull request #456 from mdimjasevic/prop-two-plurals

Properties: fix a double plural mistake
This commit is contained in:
Philip Wadler 2020-01-27 10:41:35 -06:00 committed by GitHub
commit 2a7bf78b19
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -1006,7 +1006,7 @@ _ : eval (gas 3) ⊢sucμ ≡
_ = refl
```
Similarly, we can use Agda to compute the reductions sequences given
Similarly, we can use Agda to compute the reduction sequences given
in the previous chapter. We start with the Church numeral two
applied to successor and zero. Supplying 100 steps of gas is more than enough:
```