0 | ||| Implementing `Decidable.Order.Strict` for `Data.Nat.LT`
 1 | module Data.Nat.Order.Strict
 2 |
 3 | import Data.Nat
 4 | import Decidable.Order.Strict
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | Irreflexive Nat LT where
10 |   irreflexive {x = S _} (LTESucc prf) =
11 |     irreflexive {rel = Nat.LT} prf
12 |
13 | public export
14 | Transitive Nat LT where
15 |   transitive xy yz = transitive (lteSuccRight xy) yz
16 |
17 | public export
18 | StrictPreorder Nat LT where
19 |
20 | public export
21 | decLT : (a, b : Nat) -> DecOrdering {lt = LT} a b
22 | decLT 0       0   = DecEQ Refl
23 | decLT 0     (S b) = DecLT (LTESucc LTEZero)
24 | decLT (S a)  0    = DecGT (LTESucc LTEZero)
25 | decLT (S a) (S b) = case decLT a b of
26 |   DecLT a_lt_b => DecLT (LTESucc a_lt_b)
27 |   DecEQ Refl   => DecEQ Refl
28 |   DecGT b_lt_a => DecGT (LTESucc b_lt_a)
29 |
30 | public export
31 | StrictOrdered Nat LT where
32 |   order = decLT
33 |