Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type IxList' = IxList (:~:)
- type IxEnv = IxList (IxFirst (:~:))
- class IxLift t x where
- type LiftI t x :: k
- data IxList i :: [k] -> l -> * where
- data IxFirst i :: (k, m) -> l -> * where
- data IxSecond i :: (m, k) -> l -> * where
- data IxOr i j :: Either k l -> m -> * where
- data IxJust i :: Maybe k -> l -> * where
- data IxComp i j :: k -> m -> * where
- data (k :~: a) b :: forall k. k -> k -> * where
Documentation
data IxSecond i :: (m, k) -> l -> * where Source #
IxFunctor1 k [(m, k)] (IxList k (m, k) (IxSecond m k k ((:~:) k))) (Env k m k1) Source # | |
IxFunctor1 k (m, k) (IxSecond m k k ((:~:) k)) ((:*:) k m f) Source # | |
(~) (m1, k) p ((,) m1 k (Fst m1 k p) (Snd m1 k p)) => IxLift (m1, k) m k (IxSecond m1 m k) p Source # | |
type LiftI (m1, k) m k (IxSecond m1 m k) p Source # | |
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
Category k ((:~:) k) | |
IxFunctor1 k [(m, k)] (IxList k (m, k) (IxSecond m k k ((:~:) k))) (Env k m k1) Source # | |
TestCoercion k ((:~:) k a) | |
TestEquality k ((:~:) k a) | |
(~) k a b => Known k ((:~:) k a) b Source # | |
IxFunctor1 k (m, k) (IxSecond m k k ((:~:) k)) ((:*:) k m f) Source # | |
Witness ØC ((~) k a b) ((:~:) k a b) Source # | A type equality |
(~) k a b => Bounded ((:~:) k a b) | |
(~) k a b => Enum ((:~:) k a b) | |
Eq ((:~:) k a b) | |
Ord ((:~:) k a b) | |
(~) k a b => Read ((:~:) k a b) | |
Show ((:~:) k a b) | |
type KnownC k ((:~:) k a) b Source # | |
type WitnessC ØC ((~) k a b) ((:~:) k a b) Source # | |