Mercurial > hg > Members > ryokka > HoareLogic

comparison HoareSoundness.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 e668962ac31a
children
comparison
equal deleted inserted replaced
62:bfe7d83cf9ba 63:222dd3869ab0
42 NotP : {S : Set} -> Pred S -> Pred S 42 NotP : {S : Set} -> Pred S -> Pred S
43 NotP X s = ¬ X s 43 NotP X s = ¬ X s
44 44
45 _\/_ : Cond -> Cond -> Cond 45 _\/_ : Cond -> Cond -> Cond
46 b1 \/ b2 = neg (neg b1 /\ neg b2) 46 b1 \/ b2 = neg (neg b1 /\ neg b2)
47
48 _==>_ : Cond -> Cond -> Cond
49 b1 ==> b2 = neg (b1 \/ b2)
50 47
51 when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> 48 when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) ->
52 X ⊎ Y -> Z 49 X ⊎ Y -> Z
53 when f g (inj₁ x) = f x 50 when f g (inj₁ x) = f x
54 when f g (inj₂ y) = g y 51 when f g (inj₂ y) = g y