Mercurial > hg > Members > ryokka > HoareLogic
diff RelOp.agda @ 21:5e4abc1919b4
fix module relation
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 24 Dec 2018 22:50:25 +0900 (2018-12-24) |
parents | 5001cda86c3d |
children | bfe7d83cf9ba |
line wrap: on
line diff
--- a/RelOp.agda Mon Dec 24 17:53:22 2018 +0900 +++ b/RelOp.agda Mon Dec 24 22:50:25 2018 +0900 @@ -9,22 +9,10 @@ open import Relation.Binary open import Relation.Binary.Core open import Relation.Nullary - +open import utilities module RelOp (S : Set) where -Pred : Set -> Set₁ -Pred X = X -> Set - -Imply : Set -> Set -> Set -Imply X Y = X -> Y - -Iff : Set -> Set -> Set -Iff X Y = Imply X Y × Imply Y X - -NotP : {S : Set} -> Pred S -> Pred S -NotP X s = ¬ X s - data Id {l} {X : Set} : Rel X l where ref : {x : X} -> Id x x