Closed

data Endpoint

data Closed n m

type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where ...

type Single n

type FiniteNat rhs

closed

unsafeClosed

getClosed

lowerBound

upperBound

equals

cmp

natToClosed

weakenUpper

weakenLower

strengthenUpper

strengthenLower

add

sub

multiply

isValidClosed