Data.Type.Witness.Specific.Pair

Documentation

data PairType w1 w2 t

a witness for pairs of witnesses

Constructors

MkPairType (w1 t) (w2 t)

Instances

WitnessConstraint c w2 => WitnessConstraint (c :: k -> Constraint) (PairType w1 w2 :: k -> Type)

right-biased

Defined in Data.Type.Witness.Specific.Pair

Methods

witnessConstraint :: forall (t :: k0). PairType w1 w2 t -> Dict (c t)

TestEquality w1 => TestEquality (PairType w1 w2 :: k -> Type)

left-biased

Defined in Data.Type.Witness.Specific.Pair

Methods

testEquality :: forall (a :: k0) (b :: k0). PairType w1 w2 a -> PairType w1 w2 b -> Maybe (a :~: b)

TestOrder w1 => TestOrder (PairType w1 w2 :: k -> Type)

left-biased

Defined in Data.Type.Witness.Specific.Pair

Methods

testCompare :: forall (a :: k0) (b :: k0). PairType w1 w2 a -> PairType w1 w2 b -> WOrdering a b

(Representative w1, Representative w2) => Representative (PairType w1 w2 :: k -> Type)

Defined in Data.Type.Witness.Specific.Pair

Methods

getRepWitness :: Subrepresentative (PairType w1 w2) (PairType w1 w2)

(Is w1 t, Is w2 t) => Is (PairType w1 w2 :: k -> Type) (t :: k)

Defined in Data.Type.Witness.Specific.Pair

Methods

representative :: PairType w1 w2 t