Idris2Doc
: Data.Nat.Order
Index
Default
Alternative
Black & White
Data.Nat.Order
Implementation of ordering relations for `Nat`ural numbers
decideLTE
: (n :
Nat
) -> (m :
Nat
) ->
Dec
(
LTE
n m)
Totality
: total
lte
: (m :
Nat
) -> (n :
Nat
) ->
Dec
(
LTE
m n)
Totality
: total
ltesuccinjective
:
Not
(
LTE
n m) ->
Not
(
LTE
(
S
n) (
S
m))
Totality
: total
shift
: (m :
Nat
) -> (n :
Nat
) ->
LTE
m n ->
LTE
(
S
m) (
S
n)
Totality
: total
zeroAlwaysSmaller
:
LTE
0
n
Totality
: total
zeroNeverGreater
:
Not
(
LTE
(
S
n)
0
)
Totality
: total