Safe Haskell | None |
---|---|
Language | Haskell2010 |
Closed
Synopsis
- data Endpoint
- data Closed (a :: Nat) (b :: Nat)
- type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) where ...
- type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)
- type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs
- closed :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, a <= b) => Integer -> Maybe (Closed a b)
- unsafeClosed :: forall (a :: Nat) (b :: Nat). (HasCallStack, KnownNat a, KnownNat b, a <= b) => Integer -> Closed a b
- clamp :: forall (a :: Nat) (b :: Nat) i. (Integral i, KnownNat a, KnownNat b, a <= b) => i -> Closed a b
- getClosed :: Closed a b -> Integer
- lowerBound :: forall (a :: Nat) (b :: Nat). Closed a b -> Proxy a
- upperBound :: forall (a :: Nat) (b :: Nat). Closed a b -> Proxy b
- equals :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat). Closed a b -> Closed o p -> Bool
- cmp :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat). Closed a b -> Closed o p -> Ordering
- natToClosed :: forall (a :: Nat) (b :: Nat) (x :: Nat) proxy. (KnownNat a, KnownNat b, KnownNat x, a <= x, x <= b) => proxy x -> Closed a b
- weakenUpper :: forall (k :: Nat) (a :: Nat) (b :: Nat). (a <= b, b <= k) => Closed a b -> Closed a k
- weakenLower :: forall (k :: Nat) (a :: Nat) (b :: Nat). (a <= b, k <= a) => Closed a b -> Closed k b
- strengthenUpper :: forall (k :: Nat) (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b) => Closed a b -> Maybe (Closed a k)
- strengthenLower :: forall (k :: Nat) (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b) => Closed a b -> Maybe (Closed k b)
- add :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat) (n :: Natural) (m :: Natural). Closed a b -> Closed o p -> Closed (n + o) (m + p)
- sub :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat) (n :: Natural) (m :: Natural). Closed a b -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
- multiply :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat). Closed a b -> Closed o p -> Closed (a * o) (b * p)
- isValidClosed :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Closed a b -> Bool
Documentation
Describe whether the endpoint of a Bounds
includes
or excludes its argument
data Closed (a :: Nat) (b :: Nat) Source #
Instances
type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) where ... Source #
Syntactic sugar to express open and half-open intervals using
the Closed
type
type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n) Source #
Syntactic sugar to express a value that has only one non-bottom
inhabitant using the Closed
type
type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs Source #
Syntactic sugar to express a value whose lower bound is zero
closed :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, a <= b) => Integer -> Maybe (Closed a b) Source #
Safely create a Closed
value using the specified argument
unsafeClosed :: forall (a :: Nat) (b :: Nat). (HasCallStack, KnownNat a, KnownNat b, a <= b) => Integer -> Closed a b Source #
Create a Closed
value throwing an error if the argument is not in range
clamp :: forall (a :: Nat) (b :: Nat) i. (Integral i, KnownNat a, KnownNat b, a <= b) => i -> Closed a b Source #
lowerBound :: forall (a :: Nat) (b :: Nat). Closed a b -> Proxy a Source #
Proxy for the lower bound of a Closed
value
upperBound :: forall (a :: Nat) (b :: Nat). Closed a b -> Proxy b Source #
Proxy for the upper bound of a Closed
value
equals :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat). Closed a b -> Closed o p -> Bool infix 4 Source #
Test two different types of Closed
values for equality.
cmp :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat). Closed a b -> Closed o p -> Ordering Source #
Compare two different types of Closed
values
natToClosed :: forall (a :: Nat) (b :: Nat) (x :: Nat) proxy. (KnownNat a, KnownNat b, KnownNat x, a <= x, x <= b) => proxy x -> Closed a b Source #
Convert a type-level literal into a Closed
value
weakenUpper :: forall (k :: Nat) (a :: Nat) (b :: Nat). (a <= b, b <= k) => Closed a b -> Closed a k Source #
Add inhabitants at the end
weakenLower :: forall (k :: Nat) (a :: Nat) (b :: Nat). (a <= b, k <= a) => Closed a b -> Closed k b Source #
Add inhabitants at the beginning
strengthenUpper :: forall (k :: Nat) (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b) => Closed a b -> Maybe (Closed a k) Source #
Remove inhabitants from the end. Returns Nothing
if the input was removed
strengthenLower :: forall (k :: Nat) (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b, KnownNat k, a <= b, a <= k, k <= b) => Closed a b -> Maybe (Closed k b) Source #
Remove inhabitants from the beginning. Returns Nothing
if the input was removed
add :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat) (n :: Natural) (m :: Natural). Closed a b -> Closed o p -> Closed (n + o) (m + p) Source #
Add two different types of Closed
values
sub :: forall (a :: Nat) (b :: Nat) (o :: Nat) (p :: Nat) (n :: Natural) (m :: Natural). Closed a b -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p)) Source #