Mercurial > hg > Members > ryokka > HoareLogic

changeset 64:87e125b11999

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Dec 2019 15:41:26 +0900
parents 222dd3869ab0
children bef5d4281ac8
files whileTestGears.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sun Dec 22 09:15:44 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 22 15:41:26 2019 +0900
@@ -176,6 +176,14 @@
          c10 env
       ∎
 
+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 = {!!}
+
+-- hoge : (c : ℕ ) (env : Envc ) → whileTestPwP c ( λ e s → (vari e ≡ 0) /\ (varn e ≡ c))
+-- hoge c env = GearsIdSound env (λ e → whileTestPwP c )
 
 -- induction にする
 {-# TERMINATING #-}