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

fixed imports of Collections

Browse source
This commit is contained in:
wadler 2018-05-09 19:45:15 -03:00
parent a155efa76f
commit 1cddc51221
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/TypedBarendregt.lagda
View file

@ -33,7 +33,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_) open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (¬?) open import Relation.Nullary.Negation using (¬?)
open import Collections import Collections
pattern [_] x = x ∷ [] pattern [_] x = x ∷ []
pattern [_,_] x y = x ∷ y ∷ [] pattern [_,_] x y = x ∷ y ∷ []
@ -276,7 +276,7 @@ erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M)
### Lists as sets ### Lists as sets
\begin{code} \begin{code}
open Collections.CollectionDec (Id) (_≟_) open Collections (Id) (_≟_)
\end{code} \end{code}
### Free variables ### Free variables