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

fixed build

Browse source
This commit is contained in:
wadler 2018-05-01 23:15:23 -03:00
parent 9531c60466
commit 9d5fed84a1
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Typed.lagda
View file

@ -676,6 +676,7 @@ the proof works. Bugger!
M⊆ = trans-⊆ ⊆-++₁ (trans-⊆ (⊆-++₂ {free L}) ⊆xs)
N⊆ = trans-⊆ ⊆-++₂ (trans-⊆ (⊆-++₂ {free L}) ⊆xs)
⊢rename ⊢σ ⊆xs (⊢Y ⊢M) = ⊢Y (⊢rename ⊢σ ⊆xs ⊢M)
-}
\end{code}