repos / jolie.agda.git

commit

f6b8752

parent

aace256

author

Eugene Akentyev

date

2016-12-08 16:59:23 +0400 +04

Replace lemmas with lambdas

 1@@ -137,16 +137,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
 2 check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
 3 check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
 4 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
 5-... | yes _ | no ¬p = no lem
 6-  where
 7-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
 8-    lem (t-if _ _ c₂) = ¬p c₂
 9-... | no ¬p | yes _ = no lem
10-  where
11-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
12-    lem (t-if _ c₁ _) = ¬p c₁
13-... | no _ | no ¬2 = no lem
14-  where
15-    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
16-    lem (t-if _ _ c₂) = ¬2 c₂
17+... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
18+... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
19+... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
20 check-B Γ b = {!!}