
  0 | module Data.Bounded
  1 | 
  2 | import Data.Fin
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | interface Ord b => MinBound b where
  8 |   ||| The lower bound for the type
  9 |   minBound : b
 10 | 
 11 | public export
 12 | interface Ord b => MaxBound b where
 13 |   ||| The upper bound for the type
 14 |   maxBound : b
 15 | 
 16 | public export %inline
 17 | MinBound Bits8 where
 18 |   minBound = 0x0
 19 | 
 20 | public export %inline
 21 | MaxBound Bits8 where
 22 |   maxBound = 0xff
 23 | 
 24 | public export %inline
 25 | MinBound Bits16 where
 26 |   minBound = 0x0
 27 | 
 28 | public export %inline
 29 | MaxBound Bits16 where
 30 |   maxBound = 0xffff
 31 | 
 32 | public export %inline
 33 | MinBound Bits32 where
 34 |   minBound = 0x0
 35 | 
 36 | public export %inline
 37 | MaxBound Bits32 where
 38 |   maxBound = 0xffffffff
 39 | 
 40 | public export %inline
 41 | MinBound Bits64 where
 42 |   minBound = 0x0
 43 | 
 44 | public export %inline
 45 | MaxBound Bits64 where
 46 |   maxBound = 0xffffffffffffffff
 47 | 
 48 | public export %inline
 49 | MinBound Int8 where
 50 |   minBound = (- 0x80)
 51 | 
 52 | public export %inline
 53 | MaxBound Int8 where
 54 |   maxBound = 0x7f
 55 | 
 56 | public export %inline
 57 | MinBound Int16 where
 58 |   minBound = (- 0x8000)
 59 | 
 60 | public export %inline
 61 | MaxBound Int16 where
 62 |   maxBound = 0x7fff
 63 | 
 64 | public export %inline
 65 | MinBound Int32 where
 66 |   minBound = (- 0x80000000)
 67 | 
 68 | public export %inline
 69 | MaxBound Int32 where
 70 |   maxBound = 0x7fffffff
 71 | 
 72 | public export %inline
 73 | MinBound Int64 where
 74 |   minBound = (- 0x8000000000000000)
 75 | 
 76 | public export %inline
 77 | MaxBound Int64 where
 78 |   maxBound = 0x7fffffffffffffff
 79 | 
 80 | public export %inline
 81 | MinBound Int where
 82 |   minBound = (- 0x8000000000000000)
 83 | 
 84 | public export %inline
 85 | MaxBound Int where
 86 |   maxBound = 0x7fffffffffffffff
 87 | 
 88 | public export %inline
 89 | MinBound (Fin (S n)) where
 90 |   minBound = 0
 91 | 
 92 | public export %inline
 93 | {n : _} -> MaxBound (Fin (S n)) where
 94 |   maxBound = last
 95 |