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

part1/Relations: Add _*_ import

Browse source 
For convenience, readers shouldn't worry about importing
functions that are required for exercises
This commit is contained in:
Turab Jafri 2019-08-25 23:46:15 -04:00
parent aaf5b914b0
commit bb5ff4cd64
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part1/Relations.lagda.md
View file

@ -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)
```