Mercurial > hg > Members > ryokka > HoareLogic

comparison RelOp.agda @ 21:5e4abc1919b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix module relation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Dec 2018 22:50:25 +0900
parents 5001cda86c3d
children bfe7d83cf9ba
comparison
equal deleted inserted replaced
20:fe7d6c90e435 21:5e4abc1919b4
7 open import Data.Sum 7 open import Data.Sum
8 open import Data.Unit 8 open import Data.Unit
9 open import Relation.Binary 9 open import Relation.Binary
10 open import Relation.Binary.Core 10 open import Relation.Binary.Core
11 open import Relation.Nullary 11 open import Relation.Nullary
12 12 open import utilities
13 13
14 module RelOp (S : Set) where 14 module RelOp (S : Set) where
15
16 Pred : Set -> Set₁
17 Pred X = X -> Set
18
19 Imply : Set -> Set -> Set
20 Imply X Y = X -> Y
21
22 Iff : Set -> Set -> Set
23 Iff X Y = Imply X Y × Imply Y X
24
25 NotP : {S : Set} -> Pred S -> Pred S
26 NotP X s = ¬ X s
27 15
28 data Id {l} {X : Set} : Rel X l where 16 data Id {l} {X : Set} : Rel X l where
29 ref : {x : X} -> Id x x 17 ref : {x : X} -> Id x x
30 18
31 -- substId1 | x == y & P(x) => P(y) 19 -- substId1 | x == y & P(x) => P(y)