IdrisDoc: Decidable.OrderDecidable.Order
- zeroNeverGreater : LTE (S n)
0 ->
Void
- zeroAlwaysSmaller : LTE 0
n
- shift : (m : Nat) ->
(n : Nat) ->
LTE m
n ->
LTE (S m)
(S n)
- minimum : Ordered t
to =>
t ->
t ->
t
- maximum : Ordered t
to =>
t ->
t ->
t
- ltesuccinjective : (LTE n
m ->
Void) ->
LTE (S n)
(S m) ->
Void
- lte : (m : Nat) ->
(n : Nat) ->
Dec (LTE m
n)
- decideLTE : (n : Nat) ->
(m : Nat) ->
Dec (LTE n
m)
- interface Preorder
- transitive : Preorder t
po =>
(a : t) ->
(b : t) ->
(c : t) ->
po a
b ->
po b
c ->
po a
c
- reflexive : Preorder t
po =>
(a : t) ->
po a
a
- interface Poset
- antisymmetric : Poset t
po =>
(a : t) ->
(b : t) ->
po a
b ->
po b
a ->
a =
b
- interface Ordered
- order : Ordered t
to =>
(a : t) ->
(b : t) ->
Either (to a
b)
(to b
a)
- LTEIsTransitive : (m : Nat) ->
(n : Nat) ->
(o : Nat) ->
LTE m
n ->
LTE n
o ->
LTE m
o
- LTEIsReflexive : (n : Nat) ->
LTE n
n
- LTEIsAntisymmetric : (m : Nat) ->
(n : Nat) ->
LTE m
n ->
LTE n
m ->
m =
n
- data FinLTE : Fin k ->
Fin k ->
Type
- FromNatPrf : LTE (finToNat m)
(finToNat n) ->
FinLTE m
n
- interface Equivalence
- symmetric : Equivalence t
eq =>
(a : t) ->
(b : t) ->
eq a
b ->
eq b
a
- interface Congruence
- congruent : Congruence t
f
eq =>
(a : t) ->
(b : t) ->
eq a
b ->
eq (f a)
(f b)