Properties: fix a double plural mistake

This commit is contained in:
Marko Dimjašević 2020-01-25 11:20:46 +01:00
parent 00bd32e7ac
commit 6516a5d7ba
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA

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:
```