
  0 | module Data.Refined.Nat
  1 | 
  2 | import public Data.Nat
  3 | import public Data.Refined.Core
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | fromLTE : (k,v : Nat) -> {auto 0 prf : (k <= v) === True} -> LTE k v
  9 | fromLTE 0     _     = LTEZero
 10 | fromLTE (S k) (S j) = LTESucc (fromLTE k j)
 11 | fromLTE (S k) Z impossible
 12 | 
 13 | public export
 14 | {n : Nat} -> HDec0 Nat (LTE n) where
 15 |   hdec0 v with (n <= v) proof eq
 16 |     _ | True  = Just0 (fromLTE n v)
 17 |     _ | False = Nothing0
 18 | 
 19 | public export
 20 | {n : Nat} -> HDec Nat (LTE n) where
 21 |   hdec v with (n <= v) proof eq
 22 |     _ | True  = Just (fromLTE n v)
 23 |     _ | False = Nothing
 24 | 
 25 | public export
 26 | {n : Nat} -> HDec0 Nat (`LTE` n) where
 27 |   hdec0 v with (v <= n) proof eq
 28 |     _ | True  = Just0 (fromLTE v n)
 29 |     _ | False = Nothing0
 30 | 
 31 | public export
 32 | {n : Nat} -> HDec Nat (`LTE` n) where
 33 |   hdec v with (v <= n) proof eq
 34 |     _ | True  = Just (fromLTE v n)
 35 |     _ | False = Nothing
 36 | 
 37 | public export
 38 | HDec0 Nat IsSucc where
 39 |   hdec0 0     = Nothing0
 40 |   hdec0 (S _) = Just0 %search
 41 |