Mercurial > hg > Members > ryokka > HoareLogic
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 )