Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data (k :~: a) b :: forall k. k -> k -> * where
- withRefl :: (:~:) k a b -> ((~) k a b -> r) -> r
- module Data.Proxy
- toProxy :: a -> Proxy a
- type Sized n a = Sized Vector n a
- type Sized' n a = Sized Seq n a
- coerceLength :: (n :~: m) -> Sized f n a -> Sized f m a
- type SNat n = Sing n
- sizedLength :: (ListLike (f a) a, Show (MonomorphicRep nat (Sing nat)), Integral (MonomorphicRep nat (Sing nat)), Monomorphicable nat (Sing nat), PeanoOrder nat) => Sized nat f n a -> Sing nat n
- padVecs :: forall a n m. a -> Sized' n a -> Sized' m a -> (SNat (Max n m), Sized' (Max n m) a, Sized' (Max n m) a)
- type family Flipped f a :: Nat -> Type where ...
- pattern Flipped :: forall f n a. Sized f n a -> Flipped f a n
- pattern OLt :: forall t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat t
- sNatToInt :: SNat n -> Int
Documentation
data (k :~: a) b :: forall k. k -> k -> * where infix 4 #
Propositional equality. If a :~: b
is inhabited by some terminating
value, then the type a
is the same as the type b
. To use this equality
in practice, pattern-match on the a :~: b
to get out the Refl
constructor;
in the body of the pattern-match, the compiler knows that a ~ b
.
Since: 4.7.0.0
withRefl :: (:~:) k a b -> ((~) k a b -> r) -> r #
Solves equality constraint without explicit coercion.
It has the same effect as
,
but some hacks is done to reduce runtime overhead.gcastWith
module Data.Proxy
sizedLength :: (ListLike (f a) a, Show (MonomorphicRep nat (Sing nat)), Integral (MonomorphicRep nat (Sing nat)), Monomorphicable nat (Sing nat), PeanoOrder nat) => Sized nat f n a -> Sing nat n Source #
padVecs :: forall a n m. a -> Sized' n a -> Sized' m a -> (SNat (Max n m), Sized' (Max n m) a, Sized' (Max n m) a) Source #
pattern OLt :: forall t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat t Source #