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

tiny fix to Properties

Browse source
This commit is contained in:
wadler 2018-03-07 11:55:29 -03:00
parent ea44518e27
commit b088ee59cf
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/Properties.lagda
View file

@ -14,7 +14,7 @@ by their name, properties of *inductive datatypes* are proved by
We require equivalence as in the previous chapter, plus the naturals We require equivalence as in the previous chapter, plus the naturals
and some operations upon them. We also import a couple of new operations, and some operations upon them. We also import a couple of new operations,
`cong` and `_≡⟨_⟩_`, which are explained below. `cong`, `sym`, and `_≡⟨_⟩_`, which are explained below.
\begin{code} \begin{code}
import Relation.Binary.PropositionalEquality as Eq import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym) open Eq using (_≡_; refl; cong; sym)