# HG changeset patch
# User ryokka
# Date 1576233934 -32400
# Node ID 320b765a642470872a0ef3c4950e48abb3f726b2
# Parent  7c739972cd262114aa3d55b50fefa764ce0688fb
fix loopProof

diff -r 7c739972cd26 -r 320b765a6424 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 13 19:23:15 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 13 19:45:34 2019 +0900
@@ -176,13 +176,17 @@
 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
 
 
-
-loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c))
-          → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t)
-          → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t)  → t
-loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f =
-          loopProof {!!} {!!} {!!}
-loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!}
+{-# TERMINATING #-}
+loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
+          → Pre c  → (exit : (c2 : Context) → (P c2) → Post c2  → t)
+          (f : Context → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t) → t
+loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt
+  where
+    lem : (c : Context) → t
+    lem c  with if c
+    lem c | no ¬p = f c exit
+    lem c | yes p = exit c p {!!}
+        
 
 
 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })