diff --git a/src/PropertiesAns.lagda b/src/PropertiesAns.lagda index bb9d5c98..9883bf94 100644 --- a/src/PropertiesAns.lagda +++ b/src/PropertiesAns.lagda @@ -5,7 +5,7 @@ permalink : /PropertiesAns --- \begin{code} -open import Naturals using (ℕ; suc; zero; _+_; _*_; _∸_) +open import Data.Nat using (ℕ; suc; zero; _+_; _*_; _∸_) open import Properties using (+-assoc; +-comm) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) diff --git a/src/RelationsAns.lagda b/src/RelationsAns.lagda index fd6bfdcd..83d31f30 100644 --- a/src/RelationsAns.lagda +++ b/src/RelationsAns.lagda @@ -7,7 +7,7 @@ permalink : /RelationsAns ## Imports \begin{code} -open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) +open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_) open import Relations using (_≤_; _<_; Trichotomy; even; odd) open import Properties using (+-comm; +-identity; +-suc) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)