Skip to content

Commit b22efa9

Browse files
negatratoronJefferson Carpenter
andauthored
Add imports for *-mono-<= exercise (#1080)
Co-authored-by: Jefferson Carpenter <jefferson@aoeu2code.com>
1 parent 9638790 commit b22efa9

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/plfa/part1/Relations.lagda.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ the next step is to define relations, such as _less than or equal_.
1515
```agda
1616
import Relation.Binary.PropositionalEquality as Eq
1717
open Eq using (_≡_; refl; cong)
18-
open import Data.Nat using (ℕ; zero; suc; _+_)
19-
open import Data.Nat.Properties using (+-comm; +-identityʳ)
18+
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
19+
open import Data.Nat.Properties using (+-comm; +-identityʳ; *-comm)
2020
```
2121

2222

0 commit comments

Comments
 (0)