, Data.PrimInteger

module Data.PrimInteger
import Builtin
import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order
%default total
public export
Equivalence Integer where
  Equiv x y = (prim__eq_Integer x y = 1)
  decEquiv x y with (prim__eq_Integer x y)
    decEquiv _ _ | 1 = Yes Refl
    decEquiv _ _ | _ = No  ?decEquiv
public export
Preorder Integer where
  LTE x y = (prim__lte_Integer x y = 1)
  decLTE x y with (prim__lte_Integer x y)
    decLTE _ _ | 1 = Yes Refl
    decLTE _ _ | _ = No  ?decLTE
  proofReflexivity  = believe_me ()
  proofTransitivity = believe_me ()
public export
Order Integer where
  LT x y = (prim__lt_Integer x y = 1)
  decLT x y with (prim__lt_Integer x y)
    decLT _ _ | 1 = Yes Refl
    decLT _ _ | _ = No  ?decLT

import Data.PrimInteger

public export

public export

export

public export

-- FromInteger
--
public export
fromInteger : (x : Integer) -> {auto ok : x `GTE` 0} -> Natural
fromInteger 0 = Zero
fromInteger x = case (decGTE (prim__sub_Integer x 1) 0) of
  Yes p => Succesor $ assert_total $ fromInteger $ prim__sub_Integer x 1
  No cp => void $ believe_me ()
%integerLit fromInteger
--

public export
decGTE : Preorder t => (x, y : t) -> Dec (y `LTE` x)
decGTE x y = decLTE y x

public export
decGT : Order t => (x, y : t) -> Dec (y `LT` x)
decGT x y = decLT y x