From 9d5fed84a19befe717a8a78f133a66948d99b13e Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 1 May 2018 23:15:23 -0300 Subject: [PATCH] fixed build --- src/Typed.lagda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Typed.lagda b/src/Typed.lagda index 4af31021..2058edea 100644 --- a/src/Typed.lagda +++ b/src/Typed.lagda @@ -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}