We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9638790 commit b22efa9Copy full SHA for b22efa9
1 file changed
src/plfa/part1/Relations.lagda.md
@@ -15,8 +15,8 @@ the next step is to define relations, such as _less than or equal_.
15
```agda
16
import Relation.Binary.PropositionalEquality as Eq
17
open Eq using (_≡_; refl; cong)
18
-open import Data.Nat using (ℕ; zero; suc; _+_)
19
-open import Data.Nat.Properties using (+-comm; +-identityʳ)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties using (+-comm; +-identityʳ; *-comm)
20
```
21
22
0 commit comments