michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fixed PropertiesAns and RelationsAns

Browse source
This commit is contained in:
wadler 2018-01-28 15:15:30 -02:00 committed by Wen Kokke
parent b93d1168be
commit 00b156f6cb
No known key found for this signature in database
GPG key ID: 82A1AE2526064F4B
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/PropertiesAns.lagda
View file

@ -5,7 +5,7 @@ permalink : /PropertiesAns
--- ---
\begin{code} \begin{code}
open import Naturals using (ℕ; suc; zero; _+_; _*_; _∸_) open import Data.Nat using (ℕ; suc; zero; _+_; _*_; _∸_)
open import Properties using (+-assoc; +-comm) open import Properties using (+-assoc; +-comm)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

2
src/RelationsAns.lagda
View file

@ -7,7 +7,7 @@ permalink : /RelationsAns
## Imports ## Imports
\begin{code} \begin{code}
open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
open import Relations using (_≤_; _<_; Trichotomy; even; odd) open import Relations using (_≤_; _<_; Trichotomy; even; odd)
open import Properties using (+-comm; +-identity; +-suc) open import Properties using (+-comm; +-identity; +-suc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)