Closed.Internal
data Closed n m
data Endpoint
type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: * where ...
type Single n
type FiniteNat rhs
lowerBound
upperBound
closed
unsafeClosed
unrepresentable
natToClosed
weakenUpper
weakenLower
strengthenUpper
strengthenLower
equals
cmp
add
sub
multiply
isValidClosed