{-# language DataKinds #-}
{-# language ExplicitForAll #-}
{-# language KindSignatures #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
module Arithmetic.Lt
(
zero
, substituteL
, substituteR
, incrementL
, incrementR
, weakenL
, weakenR
, plus
, transitive
, transitiveNonstrictL
, transitiveNonstrictR
, toLteL
, toLteR
, absurd
, constant
) where
import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))
import Arithmetic.Unsafe (type (<=)(Lte))
import GHC.TypeNats (CmpNat,type (+))
import qualified GHC.TypeNats as GHC
toLteR :: (a < b) -> (a + 1 <= b)
toLteR :: (a < b) -> (a + 1) <= b
toLteR a < b
Lt = (a + 1) <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
toLteL :: (a < b) -> (1 + a <= b)
toLteL :: (a < b) -> (1 + a) <= b
toLteL a < b
Lt = (1 + a) <= b
forall (a :: Nat) (b :: Nat). a <= b
Lte
substituteL :: (b :=: c) -> (b < a) -> (c < a)
substituteL :: (b :=: c) -> (b < a) -> c < a
substituteL b :=: c
Eq b < a
Lt = c < a
forall (a :: Nat) (b :: Nat). a < b
Lt
substituteR :: (b :=: c) -> (a < b) -> (a < c)
substituteR :: (b :=: c) -> (a < b) -> a < c
substituteR b :=: c
Eq a < b
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt
plus :: (a < b) -> (c <= d) -> (a + c < b + d)
plus :: (a < b) -> (c <= d) -> (a + c) < (b + d)
plus a < b
Lt c <= d
Lte = (a + c) < (b + d)
forall (a :: Nat) (b :: Nat). a < b
Lt
incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a < b) -> (c + a < c + b)
incrementL :: (a < b) -> (c + a) < (c + b)
incrementL a < b
Lt = (c + a) < (c + b)
forall (a :: Nat) (b :: Nat). a < b
Lt
incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a < b) -> (a + c < b + c)
incrementR :: (a < b) -> (a + c) < (b + c)
incrementR a < b
Lt = (a + c) < (b + c)
forall (a :: Nat) (b :: Nat). a < b
Lt
weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a < b) -> (a < c + b)
weakenL :: (a < b) -> a < (c + b)
weakenL a < b
Lt = a < (c + b)
forall (a :: Nat) (b :: Nat). a < b
Lt
weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).
(a < b) -> (a < b + c)
weakenR :: (a < b) -> a < (b + c)
weakenR a < b
Lt = a < (b + c)
forall (a :: Nat) (b :: Nat). a < b
Lt
transitive :: (a < b) -> (b < c) -> (a < c)
transitive :: (a < b) -> (b < c) -> a < c
transitive a < b
Lt b < c
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt
transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)
transitiveNonstrictR :: (a < b) -> (b <= c) -> a < c
transitiveNonstrictR a < b
Lt b <= c
Lte = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt
transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)
transitiveNonstrictL :: (a <= b) -> (b < c) -> a < c
transitiveNonstrictL a <= b
Lte b < c
Lt = a < c
forall (a :: Nat) (b :: Nat). a < b
Lt
zero :: 0 < 1
zero :: 0 < 1
zero = 0 < 1
forall (a :: Nat) (b :: Nat). a < b
Lt
absurd :: n < 0 -> void
absurd :: (n < 0) -> void
absurd n < 0
Lt = [Char] -> void
forall a. HasCallStack => [Char] -> a
error [Char]
"Arithmetic.Nat.absurd: n < 0"
constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)
constant :: a < b
constant = a < b
forall (a :: Nat) (b :: Nat). a < b
Lt