From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Thu, 8 Dec 2016 12:59:23 +0000 (+0300)
Subject: Replace lemmas with lambdas
X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=f6b87527dec4689bde6352664ac6afa2b46d47cf;p=jolie.agda.git

Replace lemmas with lambdas
---

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 07a26c5..c556b53 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -137,16 +137,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
 check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
 check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
-... | yes _ | no ¬p = no lem
-  where
-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
-    lem (t-if _ _ c₂) = ¬p c₂
-... | no ¬p | yes _ = no lem
-  where
-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
-    lem (t-if _ c₁ _) = ¬p c₁
-... | no _ | no ¬2 = no lem
-  where
-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
-    lem (t-if _ _ c₂) = ¬2 c₂
+... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
+... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
+... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
 check-B Γ b = {!!}