changeset 65:bef5d4281ac8

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Dec 2019 15:41:41 +0900
parents 87e125b11999
children 9071e5a77a13
files whileTestGears.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sun Dec 22 15:41:26 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 22 15:41:41 2019 +0900
@@ -179,8 +179,8 @@
 whileTestPwPSound :  (c : ℕ) → whileTestPwP c ( λ env s → whileTestStateP s1 env )
 whileTestPwPSound c = record { pi1 = refl ; pi2 = refl }
 
-GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → f env ( λ env s → post env )
-GearsIdSound env {post} f = {!!}
+GearsIdSound : (env : Envc) {post : Envc → Set} (f : {l : Level } {t : Set l } → Envc → ((e : Envc) → post e → t ) → t )  → post (f env ( λ env s → env ))
+GearsIdSound env {post} f = ?
 
 -- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c))
 -- hoge c env = GearsIdSound env (λ e → whileTestPwP c )