Data.Witness.Representative

Documentation

class Eq1 p where

Methods

equals1 :: forall a. p a -> p a -> Bool

Instances

Eq1 NatKind Nat

Eq1 * w => Eq1 * (ListType w)

Eq1 k (Proxy k)

isWitnessRepresentative :: Dict (Is rep a) -> rep a

class Eq1 rep => Representative rep where

Methods

getRepWitness :: forall a. rep a -> Dict (Is rep a)

Every value is an instance of Is.

Instances

Representative NatKind Nat

Representative * w => Representative * (ListType w)

Representative k (Proxy k)

withRepresentative :: forall rep r. Representative rep => (forall a. Is rep a => rep a -> r) -> forall b. rep b -> r

class Representative rep => Is rep a where

If two representatives have the same type, then they have the same value.

Methods

representative :: rep a

The representative value for type a.

Instances

Is NatKind Nat Zero

Is NatKind Nat n => Is NatKind Nat (Succ n)

Representative * w => Is * (ListType w) ()

Is k (Proxy k) a

(Is * w a, Is * (ListType w) lt) => Is * (ListType w) (a, lt)

getRepresentative :: Is rep a => a -> rep a

rerepresentative :: Is rep a => p a -> rep a

mkAny :: Is rep a => a -> Any rep

mkAnyF :: Is rep a => f a -> AnyF rep f