← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/Relations.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/Relations.agda
1
 
 
2
 
module Logic.Relations where
3
 
 
4
 
import Logic.Base
5
 
import Data.Bool
6
 
 
7
 
Rel : Set -> Set1
8
 
Rel A = A -> A -> Set
9
 
 
10
 
Reflexive : {A : Set} -> Rel A -> Set
11
 
Reflexive {A} _R_ = {x : A} -> x R x
12
 
 
13
 
Symmetric : {A : Set} -> Rel A -> Set
14
 
Symmetric {A} _R_  = {x y : A} -> x R y -> y R x
15
 
 
16
 
Transitive : {A : Set} -> Rel A -> Set
17
 
Transitive {A} _R_ = {x y z : A} -> x R y -> y R z -> x R z
18
 
 
19
 
Congruent : {A : Set} -> Rel A -> Set
20
 
Congruent {A} _R_ = (f : A -> A)(x y : A) -> x R y -> f x R f y
21
 
 
22
 
Substitutive : {A : Set} -> Rel A -> Set1
23
 
Substitutive {A} _R_ = (P : A -> Set)(x y : A) -> x R y -> P x -> P y
24
 
 
25
 
module PolyEq (_≡_ : {A : Set} -> Rel A) where
26
 
 
27
 
  Antisymmetric : {A : Set} -> Rel A -> Set
28
 
  Antisymmetric {A} _R_ = (x y : A) -> x R y -> y R x -> x ≡ y
29
 
 
30
 
module MonoEq {A : Set}(_≡_ : Rel A) where
31
 
 
32
 
  Antisymmetric : Rel A -> Set
33
 
  Antisymmetric _R_ = (x y : A) -> x R y -> y R x -> x ≡ y
34
 
 
35
 
open Logic.Base
36
 
 
37
 
Total : {A : Set} -> Rel A -> Set
38
 
Total {A} _R_ = (x y : A) -> (x R y) \/ (y R x)
39
 
 
40
 
Decidable : (P : Set) -> Set
41
 
Decidable P = P \/ ¬ P
42