Removed an unnecessary import
This commit is contained in:
parent
1d44a3906a
commit
4e3a2734dd
1 changed files with 1 additions and 1 deletions
|
@ -18,7 +18,7 @@ the next step is to define relations, such as _less than or equal_.
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_)
|
||||
open import Data.Nat.Properties using (+-comm)
|
||||
```
|
||||
|
||||
|
|
Loading…
Reference in a new issue