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

fixing colliding definitions of \notin

Browse source
This commit is contained in:
wadler 2018-05-15 10:38:52 -03:00
parent 54eb41836f
commit 1298e7a2e8
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/TypedBarendregt.lagda
View file

@ -276,7 +276,7 @@ erase-lemma (⊢Y ⊢M) = cong `Y_ (erase-lemma ⊢M)
### Lists as sets
\begin{code}
open Collections (Id) (_≟_)
open Collections (Id) (_≟_) hiding (_∉_)
\end{code}
### Free variables