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

fixed all imports of Collections

Browse source
This commit is contained in:
wadler 2018-05-09 19:19:58 -03:00
parent 8afc6f9ce0
commit ece27d766a
2 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Acknowledgements.lagda
View file

@ -17,13 +17,15 @@ To Andreas Abel and Ulf Norell, ditto.
To David Darais, for showing me how much more compact it is to avoid raw terms. To David Darais, for showing me how much more compact it is to avoid raw terms.
For pull requests. For pull requests.
* Jonathan Prieto-Cubides
* Vikraman Choudhury * Vikraman Choudhury
* Anish Tondwalkar * Phil de Joux
* koo5
* Juhana Laurinharju
* Jonathan Prieto-Cubides
* Anish Tondwalkar
For answering questions on the Agda mailing list. For answering questions on the Agda mailing list.
* Guillaume Allais <guillaume.allais@ens-lyon.org> * Guillaume Allais <guillaume.allais@ens-lyon.org>
* Sabry, Amr A. <sabry@indiana.edu>
* Nils Anders Danielsson <nad@cse.gu.se> * Nils Anders Danielsson <nad@cse.gu.se>
* Miëtek Bak <mietek@bak.io> * Miëtek Bak <mietek@bak.io>
* Gergő Érdi <gergo@erdi.hu> * Gergő Érdi <gergo@erdi.hu>
@ -34,6 +36,7 @@ For answering questions on the Agda mailing list.
* Liam O'Connor <liamoc@cse.unsw.edu.au> * Liam O'Connor <liamoc@cse.unsw.edu.au>
* N. Raghavendra <nyraghu27132@gmail.com> * N. Raghavendra <nyraghu27132@gmail.com>
* Roman <effectfully@gmail.com> * Roman <effectfully@gmail.com>
* Amr A. Sabry <sabry@indiana.edu>
For comments on the text. For comments on the text.
* [your name goes here] * [your name goes here]

4
src/TypedBadfix.lagda
View file

@ -29,7 +29,7 @@ open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contraposition; ¬?) open import Relation.Nullary.Negation using (contraposition; ¬?)
open import Relation.Nullary.Product using (_×-dec_) open import Relation.Nullary.Product using (_×-dec_)
open import Collections using (_↔_) import Collections
\end{code} \end{code}
@ -219,7 +219,7 @@ erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lem
### 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