{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
module Arithmetic.Lte
(
zero
, reflexive
, reflexive#
, substituteL
, substituteR
, incrementL
, incrementL#
, incrementR
, incrementR#
, decrementL
, decrementL#
, decrementR
, decrementR#
, weakenL
, weakenL#
, weakenR
, weakenR#
, transitive
, transitive#
, plus
, plus#
, fromStrict
, fromStrict#
, fromStrictSucc
, fromStrictSucc#
, constant
, lift
, unlift
) where
import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#))
import GHC.TypeNats (CmpNat, type (+))
import qualified GHC.TypeNats as GHC
substituteL :: (b :=: c) -> (b <= a) -> (c <= a)
{-# INLINE substituteL #-}
substituteL :: forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (b <= a) -> c <= a
substituteL b :=: c
Eq b <= a
Lte = c <= a
forall (a :: Nat) (b :: Nat). a <= b
Lte
substituteR :: (b :=: c) -> (a <= b) -> (a <= c)
{-# INLINE substituteR #-}
substituteR :: forall (b :: Nat) (c :: Nat) (a :: Nat).
(b :=: c) -> (a <= b) -> a <= c
substituteR b :=: c
Eq a <= b
Lte = a <= c
forall (a :: Nat) (b :: Nat). a <= b
Lte
plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)
{-# INLINE plus #-}
plus :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a <= b) -> (c <= d) -> (a + c) <= (b + d)
plus a <= b
Lte c <= d
Lte = (a + c) <= (b + d)
forall (a :: Nat) (b :: Nat). a <= b
Lte
plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d)
{-# INLINE plus# #-}
plus# :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat).
(a <=# b) -> (c <=# d) -> (a + c) <=# (b + d)
plus# a <=# b
_ c <=# d
_ = (# #) -> (a + c) <=# (b + d)
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
transitive :: (a <= b) -> (b <= c) -> (a <= c)
{-# INLINE transitive #-}
transitive :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(a <= b) -> (b <= c) -> a <= c
transitive a <= b
Lte b <= c
Lte = a <= c
forall (a :: Nat) (b :: Nat). a <= b
Lte
transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c)
{-# INLINE transitive# #-}
transitive# :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(a <=# b) -> (b <=# c) -> a <=# c
transitive# a <=# b
_ b <=# c
_ = (# #) -> a <=# c
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
reflexive :: a <= a
{-# INLINE reflexive #-}
reflexive :: forall (a :: Nat). a <= a
reflexive = a <= a
forall (a :: Nat) (b :: Nat). a <= b
Lte
reflexive# :: (# #) -> a <=# a
{-# INLINE reflexive# #-}
reflexive# :: forall (a :: Nat). (# #) -> a <=# a
reflexive# (# #)
_ = (# #) -> a <=# a
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
incrementL ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <= b) ->
(c + a <= c + b)
{-# INLINE incrementL #-}
incrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat).
(a <= b) -> (c + a) <= (c + b)
incrementL a <= b
Lte = (c + a) <= (c + b)
forall (a :: Nat) (b :: Nat). a <= b
Lte
incrementL# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <=# b) ->
(c + a <=# c + b)
{-# INLINE incrementL# #-}
incrementL# :: forall (c :: Nat) (a :: Nat) (b :: Nat).
(a <=# b) -> (c + a) <=# (c + b)
incrementL# a <=# b
_ = (# #) -> (c + a) <=# (c + b)
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
incrementR ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <= b) ->
(a + c <= b + c)
{-# INLINE incrementR #-}
incrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat).
(a <= b) -> (a + c) <= (b + c)
incrementR a <= b
Lte = (a + c) <= (b + c)
forall (a :: Nat) (b :: Nat). a <= b
Lte
incrementR# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <=# b) ->
(a + c <=# b + c)
{-# INLINE incrementR# #-}
incrementR# :: forall (c :: Nat) (a :: Nat) (b :: Nat).
(a <=# b) -> (a + c) <=# (b + c)
incrementR# a <=# b
_ = (# #) -> (a + c) <=# (b + c)
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
weakenL ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <= b) ->
(a <= c + b)
{-# INLINE weakenL #-}
weakenL :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (c + b)
weakenL a <= b
Lte = a <= (c + b)
forall (a :: Nat) (b :: Nat). a <= b
Lte
weakenL# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <=# b) ->
(a <=# c + b)
{-# INLINE weakenL# #-}
weakenL# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <=# b) -> a <=# (c + b)
weakenL# a <=# b
_ = (# #) -> a <=# (c + b)
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
weakenR ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <= b) ->
(a <= b + c)
{-# INLINE weakenR #-}
weakenR :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <= b) -> a <= (b + c)
weakenR a <= b
Lte = a <= (b + c)
forall (a :: Nat) (b :: Nat). a <= b
Lte
weakenR# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a <=# b) ->
(a <=# b + c)
{-# INLINE weakenR# #-}
weakenR# :: forall (c :: Nat) (a :: Nat) (b :: Nat). (a <=# b) -> a <=# (b + c)
weakenR# a <=# b
_ = (# #) -> a <=# (b + c)
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
decrementL ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(c + a <= c + b) ->
(a <= b)
{-# INLINE decrementL #-}
decrementL :: forall (c :: Nat) (a :: Nat) (b :: Nat).
((c + a) <= (c + b)) -> a <= b
decrementL (c + a) <= (c + b)
Lte = a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
decrementL# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(c + a <=# c + b) ->
(a <=# b)
{-# INLINE decrementL# #-}
decrementL# :: forall (c :: Nat) (a :: Nat) (b :: Nat).
((c + a) <=# (c + b)) -> a <=# b
decrementL# (c + a) <=# (c + b)
_ = (# #) -> a <=# b
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
decrementR ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a + c <= b + c) ->
(a <= b)
{-# INLINE decrementR #-}
decrementR :: forall (c :: Nat) (a :: Nat) (b :: Nat).
((a + c) <= (b + c)) -> a <= b
decrementR (a + c) <= (b + c)
Lte = a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
decrementR# ::
forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a + c <=# b + c) ->
(a <=# b)
{-# INLINE decrementR# #-}
decrementR# :: forall (c :: Nat) (a :: Nat) (b :: Nat).
((a + c) <=# (b + c)) -> a <=# b
decrementR# (a + c) <=# (b + c)
_ = (# #) -> a <=# b
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
fromStrict :: (a < b) -> (a <= b)
{-# INLINE fromStrict #-}
fromStrict :: forall (a :: Nat) (b :: Nat). (a < b) -> a <= b
fromStrict a < b
Lt = a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
fromStrict# :: (a <# b) -> (a <=# b)
{-# INLINE fromStrict# #-}
fromStrict# :: forall (a :: Nat) (b :: Nat). (a <# b) -> a <=# b
fromStrict# a <# b
_ = (# #) -> a <=# b
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
fromStrictSucc :: (a < b) -> (a + 1 <= b)
{-# INLINE fromStrictSucc #-}
fromStrictSucc :: forall (a :: Nat) (b :: Nat). (a < b) -> (a + 1) <= b
fromStrictSucc a < b
Lt = (a + 1) <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
fromStrictSucc# :: (a <# b) -> (a + 1 <=# b)
{-# INLINE fromStrictSucc# #-}
fromStrictSucc# :: forall (a :: Nat) (b :: Nat). (a <# b) -> (a + 1) <=# b
fromStrictSucc# a <# b
_ = (# #) -> (a + 1) <=# b
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
zero :: 0 <= a
{-# INLINE zero #-}
zero :: forall (a :: Nat). 0 <= a
zero = 0 <= a
forall (a :: Nat) (b :: Nat). a <= b
Lte
constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)
{-# INLINE constant #-}
constant :: forall (a :: Nat) (b :: Nat).
(IsLte (CmpNat a b) ~ 'True) =>
a <= b
constant = a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
type family IsLte (o :: Ordering) :: Bool where
IsLte 'GT = 'False
IsLte 'LT = 'True
IsLte 'EQ = 'True
unlift :: (a <= b) -> (a <=# b)
unlift :: forall (a :: Nat) (b :: Nat). (a <= b) -> a <=# b
unlift a <= b
_ = (# #) -> a <=# b
forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
Lte# (# #)
lift :: (a <=# b) -> (a <= b)
lift :: forall (a :: Nat) (b :: Nat). (a <=# b) -> a <= b
lift a <=# b
_ = a <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte