git.iko.soy/Idris-dev
on master help sign in
Documentation improvement
1139e72Jan Bessai
libs/base/Decidable/Order.idr+14−10
compare with master
unifiedsplit
@@ -10,7 +10,7 @@ import Decidable.Equality
10--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
11
11
12--------------------------------------------------------------------------------
12--------------------------------------------------------------------------------
13−-- Preorders and Posets
13+-- Preorders, Posets and total Orders
14--------------------------------------------------------------------------------
14--------------------------------------------------------------------------------
15
15
16class Preorder t (po : t -> t -> Type) where
16class Preorder t (po : t -> t -> Type) where
@@ -23,6 +23,16 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
24 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
24 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
25
25
26+minimum : (Ordered t to) => t -> t -> t
27+minimum x y with (order x y)
28+ | Left _ = x
29+ | Right _ = y
30+
31+maximum : (Ordered t to) => t -> t -> t
32+maximum x y with (order x y)
33+ | Left _ = y
34+ | Right _ = x
35+
26--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
27-- Natural numbers
37-- Natural numbers
28--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
@@ -101,15 +111,9 @@ instance Ordered Nat NatLTE where
101 order (S k) (S j) | Left prf = Left (shift k j prf)
111 order (S k) (S j) | Left prf = Left (shift k j prf)
102 order (S k) (S j) | Right prf = Right (shift j k prf)
112 order (S k) (S j) | Right prf = Right (shift j k prf)
103
113
104−minimum : (Ordered t to) => t -> t -> t
114+--------------------------------------------------------------------------------
105−minimum x y with (order x y)
115+-- Finite numbers
106− | Left _ = x
116+--------------------------------------------------------------------------------
107− | Right _ = y
108−
109−maximum : (Ordered t to) => t -> t -> t
110−maximum x y with (order x y)
111− | Left _ = y
112− | Right _ = x
113
117
114using (k : Nat)
118using (k : Nat)
115 data FinLTE : Fin k -> Fin k -> Type where
119 data FinLTE : Fin k -> Fin k -> Type where