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 = 0} _ impossible
11 |   irreflexive {x = S _} (LTESucc prf) =
12 |     irreflexive {rel = Nat.LT} prf
13 |
14 | public export
15 | Transitive Nat LT where
16 |   transitive xy yz = transitive (lteSuccRight xy) yz
17 |
18 | public export
19 | StrictPreorder Nat LT where
20 |
21 | public export
22 | decLT : (a, b : Nat) -> DecOrdering {lt = LT} a b
23 | decLT 0       0   = DecEQ Refl
24 | decLT 0     (S b) = DecLT (LTESucc LTEZero)
25 | decLT (S a)  0    = DecGT (LTESucc LTEZero)
26 | decLT (S a) (S b) = case decLT a b of
27 |   DecLT a_lt_b => DecLT (LTESucc a_lt_b)
28 |   DecEQ Refl   => DecEQ Refl
29 |   DecGT b_lt_a => DecGT (LTESucc b_lt_a)
30 |
31 | public export
32 | StrictOrdered Nat LT where
33 |   order = decLT
34 |