Mercurial > hg > Members > ryokka > HoareLogic

diff whileTestPrimProof.agda @ 63:222dd3869ab0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove wrong ==>
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Dec 2019 09:15:44 +0900
parents 62dcb0ae2c94
children 9071e5a77a13
line wrap: on
line diff
--- a/whileTestPrimProof.agda	Sat Dec 21 21:12:07 2019 +0900
+++ b/whileTestPrimProof.agda	Sun Dec 22 09:15:44 2019 +0900
@@ -207,9 +207,6 @@
 _\/_ : Cond -> Cond -> Cond
 b1 \/ b2 = neg (neg b1 /\ neg b2)
 
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
 SemCond : Cond -> State -> Set
 SemCond c p = c p ≡ true