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

fixes in fresh

Browse source
This commit is contained in:
wadler 2018-06-30 22:45:32 -03:00
parent ec049e109a
commit deeb5269f6
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
extra/fresh/Collections.lagda
View file

@ -21,7 +21,6 @@ open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Isomorphism using (_≃_)
open import Function using (_∘_)
open import Level using (Level)
open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
@ -40,7 +39,7 @@ open import Relation.Nullary.Product using (_×-dec_)
\begin{code}
module fresh.Collections (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
Coll : Set → Set
Coll A = List A

4
extra/fresh/TypedFresh.lagda
View file

@ -26,7 +26,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 (¬?)
import Collections
import fresh.Collections
pattern [_] w = w ∷ []
pattern [_,_] w x = w ∷ x ∷ []
@ -268,7 +268,7 @@ erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M)
### Lists as sets
\begin{code}
open Collections (Id) (_≟_)
open fresh.Collections (Id) (_≟_)
\end{code}
### Free variables