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