Mercurial > hg > Members > ryokka > HoareLogic

diff whileTestPrimProof.agda @ 66:9071e5a77a13

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
implies
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Dec 2019 09:48:54 +0900
parents 222dd3869ab0
children a7263ecf8671
line wrap: on
line diff
--- a/whileTestPrimProof.agda	Sun Dec 22 15:41:41 2019 +0900
+++ b/whileTestPrimProof.agda	Mon Dec 23 09:48:54 2019 +0900
@@ -250,6 +250,8 @@
 PrimSemComm : ∀ {l} -> PrimComm -> Rel State l
 PrimSemComm prim s1 s2 =  Id State (prim s1) s2
 
+
+
 axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) ->
                   (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) ->
                   SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2