module Data.Witness
(
module Data.Proxy,
module Data.Type.Equality,
module Data.Witness.Any,
module Data.Witness.WitnessDict,
module Data.Witness.WitnessFDict,
module Data.Witness.Nat,
module Data.Witness.ListElement,
module Data.Witness.List,
module Data.Witness.Representative,
module Data.Witness
) where
{
import Data.Proxy;
import Data.Type.Equality;
import Data.Witness.Any;
import Data.Witness.WitnessDict;
import Data.Witness.WitnessFDict;
import Data.Witness.Nat;
import Data.Witness.ListElement;
import Data.Witness.List;
import Data.Witness.Representative;
;
matchIs :: forall w a b. (TestEquality w,Is w a,Is w b) => Proxy w -> Maybe (a :~: b);
matchIs _ = testEquality r r where
{
r :: forall t. (Is w t) => w t;
r = representative;
};
}