Mercurial > hg > Members > ryokka > HoareLogic

diff whileTestPrimProof.agda @ 24:e668962ac31a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rename modules
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:45:06 +0900
parents 3968822b9693
children 62dcb0ae2c94
line wrap: on
line diff
--- a/whileTestPrimProof.agda	Tue Dec 25 08:41:15 2018 +0900
+++ b/whileTestPrimProof.agda	Tue Dec 25 08:45:06 2018 +0900
@@ -10,7 +10,7 @@
 open import utilities hiding ( _/\_ )
 open import whileTestPrim
 
-open import HoareData PrimComm Cond Axiom Tautology _and_ neg
+open import Hoare PrimComm Cond Axiom Tautology _and_ neg
 
 open Env
 
@@ -261,7 +261,7 @@
 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
 
-open import Hoare
+open import HoareSoundness
     Cond 
     PrimComm 
     neg