# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595035963 -32400
# Node ID 07b183a726f67787a0face55a3055a84da3cb32a
# Parent  77798ab0e660255c1b7efa2c0a8d02f546aee6ba
...

diff -r 77798ab0e660 -r 07b183a726f6 utilities.agda
--- a/utilities.agda	Sat Jan 11 22:09:49 2020 +0900
+++ b/utilities.agda	Sat Jul 18 10:32:43 2020 +0900
@@ -4,7 +4,7 @@
 open import Function
 open import Data.Nat
 open import Data.Product
-open import Data.Bool hiding ( _≟_  ; _≤?_)
+open import Data.Bool  hiding ( _≟_ ) --  ; _≤?_)
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
diff -r 77798ab0e660 -r 07b183a726f6 whileTestGears.agda
--- a/whileTestGears.agda	Sat Jan 11 22:09:49 2020 +0900
+++ b/whileTestGears.agda	Sat Jul 18 10:32:43 2020 +0900
@@ -2,7 +2,7 @@
 
 open import Function
 open import Data.Nat
-open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
+open import Data.Bool hiding ( _≟_ ) -- ; _≤?_ ; _≤_ ; _<_)
 open import Data.Product
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
diff -r 77798ab0e660 -r 07b183a726f6 whileTestGears1.agda
--- a/whileTestGears1.agda	Sat Jan 11 22:09:49 2020 +0900
+++ b/whileTestGears1.agda	Sat Jul 18 10:32:43 2020 +0900
@@ -16,6 +16,13 @@
     vari : ℕ
 open Env
 
+whileTestS : { m : Level}  -> (c10 : ℕ) → (Code : Env -> Set m) -> Set m
+whileTestS c10 next = next (record {varn = c10 ; vari = 0} )
+
+whileTestS1 :  (c10 : ℕ) →  whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) )
+whileTestS1 c10 = record { pi1 = refl ; pi2 = refl }
+
+
 whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t
 whileTest c10 next = next (record {varn = c10 ; vari = 0} )
 
diff -r 77798ab0e660 -r 07b183a726f6 whileTestPrim.agda
--- a/whileTestPrim.agda	Sat Jan 11 22:09:49 2020 +0900
+++ b/whileTestPrim.agda	Sat Jul 18 10:32:43 2020 +0900
@@ -39,11 +39,11 @@
 
 program : ℕ → Comm
 program c10 = 
-    Seq ( PComm (λ env → record env {varn = c10}))
-    $ Seq ( PComm (λ env → record env {vari = 0}))
-    $ While (λ env → lt zero (varn env ) )
-      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
-        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
+    Seq ( PComm (λ env → record env {varn = c10}))                     ---    n = c10 ;
+    $ Seq ( PComm (λ env → record env {vari = 0}))                     ---    i = 0 ;
+    $ While (λ env → lt zero (varn env ) )                             ---    while ( 0 < n ) {
+      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))     ---        i = i + 1
+        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))       ---        n = n - 1 }
 
 simple : ℕ → Comm
 simple c10 =