Safe Haskell	None
Language	GHC2021

Control.Category.NatOrd

Synopsis

data (n :: Nat) :<=: (m :: Nat) where
- ReflLE :: forall (n :: Nat). n :<=: n
- SuccLE :: forall (n :: Nat) (n1 :: Natural). !(n :<=: n1) -> n :<=: (1 + n1)
type (:>=:) = Dual (:<=:)
data Finite' (n :: Natural) where
- Finite' :: forall (m :: Nat) (n1 :: Natural). (m :<=: n1) -> Finite' (1 + n1)
shift' :: forall (n :: Natural). Finite' n -> Finite' (1 + n)
fromFinite :: forall (n :: Nat). KnownNat n => Finite n -> Finite' n
toFinite :: forall (n :: Nat). KnownNat n => Finite' n -> Finite n

Documentation

data (n :: Nat) :<=: (m :: Nat) where infix 4 Source #

Inductively defined "less than or equals" relation

Constructors

ReflLE :: forall (n :: Nat). n :<=: n
SuccLE :: forall (n :: Nat) (n1 :: Natural). !(n :<=: n1) -> n :<=: (1 + n1)

Instances details

Category (:<=:) Source #
Instance details Defined in Control.Category.NatOrd Methods id :: forall (a :: Nat). a :<=: a # (.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :<=: c) -> (a :<=: b) -> a :<=: c #

"greater than or equals"

Given a type-level n :: Nat, Finite' n is the collection of all values of type m :<=: n for some m :: Nat.

Constructors

Finite' :: forall (m :: Nat) (n1 :: Natural). (m :<=: n1) -> Finite' (1 + n1)