Proof.Equational

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

Constructors

Refl :: (:~:) k a a

Instances

Equality k ((:=:) k)

Methods

symmetry :: eq a b -> eq b a

Preorder k ((:=:) k)

Methods

reflexivity :: Sing ((:=:) k) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

TestEquality k ((:~:) k a)

Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b)

(~) k a b => Bounded ((:~:) k a b)

Methods

minBound :: (k :~: a) b

maxBound :: (k :~: a) b

(~) k a b => Enum ((:~:) k a b)

Methods

succ :: (k :~: a) b -> (k :~: a) b

pred :: (k :~: a) b -> (k :~: a) b

toEnum :: Int -> (k :~: a) b

fromEnum :: (k :~: a) b -> Int

enumFrom :: (k :~: a) b -> [(k :~: a) b]

enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

Eq ((:~:) k a b)

Methods

(==) :: (k :~: a) b -> (k :~: a) b -> Bool

(/=) :: (k :~: a) b -> (k :~: a) b -> Bool

((~) * a b, Data a) => Data ((:~:) * a b)

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> (* :~: a) b -> c ((* :~: a) b)

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((* :~: a) b)

toConstr :: (* :~: a) b -> Constr

dataTypeOf :: (* :~: a) b -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ((* :~: a) b))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ((* :~: a) b))

gmapT :: (forall c. Data c => c -> c) -> (* :~: a) b -> (* :~: a) b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (* :~: a) b -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (* :~: a) b -> r

gmapQ :: (forall d. Data d => d -> u) -> (* :~: a) b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (* :~: a) b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b)

Ord ((:~:) k a b)

Methods

compare :: (k :~: a) b -> (k :~: a) b -> Ordering

(<) :: (k :~: a) b -> (k :~: a) b -> Bool

(<=) :: (k :~: a) b -> (k :~: a) b -> Bool

(>) :: (k :~: a) b -> (k :~: a) b -> Bool

(>=) :: (k :~: a) b -> (k :~: a) b -> Bool

max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b

min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b

(~) k a b => Read ((:~:) k a b)

Methods

readsPrec :: Int -> ReadS ((k :~: a) b)

readList :: ReadS [(k :~: a) b]

readPrec :: ReadPrec ((k :~: a) b)

readListPrec :: ReadPrec [(k :~: a) b]

Show ((:~:) k a b)

Methods

showsPrec :: Int -> (k :~: a) b -> ShowS

show :: (k :~: a) b -> String

showList :: [(k :~: a) b] -> ShowS

type (:=:) = (:~:) infix 4

sym :: (:~:) k a b -> (:~:) k b a

Symmetry of equality

trans :: (:~:) k a b -> (:~:) k b c -> (:~:) k a c

Transitivity of equality

class Preorder eq => Equality eq where

Minimal complete definition

symmetry

Methods

symmetry :: eq a b -> eq b a

Instances

Equality k (Leibniz k)

Methods

symmetry :: eq a b -> eq b a

Equality k ((:=:) k)

Methods

symmetry :: eq a b -> eq b a

class Preorder eq where

Minimal complete definition

reflexivity, transitivity

Methods

reflexivity :: Sing a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Instances

Preorder k (Leibniz k)

Methods

reflexivity :: Sing (Leibniz k) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Preorder k ((:=:) k)

Methods

reflexivity :: Sing ((:=:) k) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Preorder * (->)

Methods

reflexivity :: Sing (->) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

reflexivity' :: (SingI x, Preorder r) => r x x

type (:\/:) a b = Either a b infixr 2

type (:/\:) a b = (a, b) infixr 3

(=<=) :: Preorder r => r x y -> Reason r y z -> r x z infixl 4

(=>=) :: Preorder r => r y z -> Reason r x y -> r x z infixl 4

(=~=) :: Preorder r => r x y -> Sing y -> r x y infixl 4

data Leibniz a b

Constructors

Leibniz

Fields

• apply :: forall f. f a -> f b

Instances

Equality k (Leibniz k)

Methods

symmetry :: eq a b -> eq b a

Preorder k (Leibniz k)

Methods

reflexivity :: Sing (Leibniz k) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

data Reason eq x y where

Constructors

Because :: Sing y -> eq x y -> Reason eq x y infix 5

because :: Sing y -> eq x y -> Reason eq x y infix 5

by :: Sing y -> eq x y -> Reason eq x y

(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z infixl 4

start :: Preorder eq => Sing a -> eq a a

byDefinition :: (SingI a, Preorder eq) => eq a a

admitted :: Reason eq x y

Warning: There are some goals left yet unproven.

data Proxy k t :: forall k. k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Methods

(>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b

(>>) :: Proxy * a -> Proxy * b -> Proxy * b

return :: a -> Proxy * a

fail :: String -> Proxy * a

Functor (Proxy *)

Methods

fmap :: (a -> b) -> Proxy * a -> Proxy * b

(<$) :: a -> Proxy * b -> Proxy * a

Applicative (Proxy *)

Methods

pure :: a -> Proxy * a

(<*>) :: Proxy * (a -> b) -> Proxy * a -> Proxy * b

(*>) :: Proxy * a -> Proxy * b -> Proxy * b

(<*) :: Proxy * a -> Proxy * b -> Proxy * a

Foldable (Proxy *)

Methods

fold :: Monoid m => Proxy * m -> m

foldMap :: Monoid m => (a -> m) -> Proxy * a -> m

foldr :: (a -> b -> b) -> b -> Proxy * a -> b

foldr' :: (a -> b -> b) -> b -> Proxy * a -> b

foldl :: (b -> a -> b) -> b -> Proxy * a -> b

foldl' :: (b -> a -> b) -> b -> Proxy * a -> b

foldr1 :: (a -> a -> a) -> Proxy * a -> a

foldl1 :: (a -> a -> a) -> Proxy * a -> a

toList :: Proxy * a -> [a]

null :: Proxy * a -> Bool

length :: Proxy * a -> Int

elem :: Eq a => a -> Proxy * a -> Bool

maximum :: Ord a => Proxy * a -> a

minimum :: Ord a => Proxy * a -> a

sum :: Num a => Proxy * a -> a

product :: Num a => Proxy * a -> a

Traversable (Proxy *)

Methods

traverse :: Applicative f => (a -> f b) -> Proxy * a -> f (Proxy * b)

sequenceA :: Applicative f => Proxy * (f a) -> f (Proxy * a)

mapM :: Monad m => (a -> m b) -> Proxy * a -> m (Proxy * b)

sequence :: Monad m => Proxy * (m a) -> m (Proxy * a)

Generic1 (Proxy *)

Associated Types

type Rep1 (Proxy * :: * -> *) :: * -> *

Methods

from1 :: Proxy * a -> Rep1 (Proxy *) a

to1 :: Rep1 (Proxy *) a -> Proxy * a

Alternative (Proxy *)

Methods

empty :: Proxy * a

(<|>) :: Proxy * a -> Proxy * a -> Proxy * a

some :: Proxy * a -> Proxy * [a]

many :: Proxy * a -> Proxy * [a]

MonadPlus (Proxy *)

Methods

mzero :: Proxy * a

mplus :: Proxy * a -> Proxy * a -> Proxy * a

Bounded (Proxy k s)

Methods

minBound :: Proxy k s

maxBound :: Proxy k s

Enum (Proxy k s)

Methods

succ :: Proxy k s -> Proxy k s

pred :: Proxy k s -> Proxy k s

toEnum :: Int -> Proxy k s

fromEnum :: Proxy k s -> Int

enumFrom :: Proxy k s -> [Proxy k s]

enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s]

Eq (Proxy k s)

Methods

(==) :: Proxy k s -> Proxy k s -> Bool

(/=) :: Proxy k s -> Proxy k s -> Bool

Data t => Data (Proxy * t)

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy * t -> c (Proxy * t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy * t)

toConstr :: Proxy * t -> Constr

dataTypeOf :: Proxy * t -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Proxy * t))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Proxy * t))

gmapT :: (forall b. Data b => b -> b) -> Proxy * t -> Proxy * t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy * t -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy * t -> r

gmapQ :: (forall d. Data d => d -> u) -> Proxy * t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy * t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy * t -> m (Proxy * t)

Ord (Proxy k s)

Methods

compare :: Proxy k s -> Proxy k s -> Ordering

(<) :: Proxy k s -> Proxy k s -> Bool

(<=) :: Proxy k s -> Proxy k s -> Bool

(>) :: Proxy k s -> Proxy k s -> Bool

(>=) :: Proxy k s -> Proxy k s -> Bool

max :: Proxy k s -> Proxy k s -> Proxy k s

min :: Proxy k s -> Proxy k s -> Proxy k s

Read (Proxy k s)

Methods

readsPrec :: Int -> ReadS (Proxy k s)

readList :: ReadS [Proxy k s]

readPrec :: ReadPrec (Proxy k s)

readListPrec :: ReadPrec [Proxy k s]

Show (Proxy k s)

Methods

showsPrec :: Int -> Proxy k s -> ShowS

show :: Proxy k s -> String

showList :: [Proxy k s] -> ShowS

Ix (Proxy k s)

Methods

range :: (Proxy k s, Proxy k s) -> [Proxy k s]

index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool

rangeSize :: (Proxy k s, Proxy k s) -> Int

unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int

Generic (Proxy k t)

Associated Types

type Rep (Proxy k t) :: * -> *

Methods

from :: Proxy k t -> Rep (Proxy k t) x

to :: Rep (Proxy k t) x -> Proxy k t

Semigroup (Proxy k s)

Methods

(<>) :: Proxy k s -> Proxy k s -> Proxy k s

sconcat :: NonEmpty (Proxy k s) -> Proxy k s

stimes :: Integral b => b -> Proxy k s -> Proxy k s

Monoid (Proxy k s)

Methods

mempty :: Proxy k s

mappend :: Proxy k s -> Proxy k s -> Proxy k s

mconcat :: [Proxy k s] -> Proxy k s

type Rep1 (Proxy *)

type Rep1 (Proxy *) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

type Rep (Proxy k t)

type Rep (Proxy k t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

cong :: forall f a b. Proxy f -> (a :=: b) -> f a :=: f b

cong' :: (Sing m -> Sing (f m)) -> (a :=: b) -> f a :=: f b

class Proposition f where

Minimal complete definition

unWrap, wrap

Associated Types

type OriginalProp (f :: k -> *) (n :: k) :: *

Methods

unWrap :: f n -> OriginalProp f n

wrap :: OriginalProp f n -> f n

data HVec xs where

Constructors

HNil :: HVec '[]

(:-) :: x -> HVec xs -> HVec (x ': xs) infixr 9

class FromBool c where

Minimal complete definition

fromBool

Associated Types

type Predicate c :: Bool

type Args c :: [*]

Methods

fromBool :: Predicate c ~ True => HVec (Args c) -> c

applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c

applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c

fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ True) => proxy c -> Args c :~> c

Conversion between equalities

fromRefl :: (Preorder eq, SingI b) => (a :=: b) -> eq a b

fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b

reflToLeibniz :: (a :=: b) -> Leibniz a b

leibnizToRefl :: Leibniz a b -> a :=: b

Coercion

coerce :: (a :=: b) -> f a -> f b

Type coercion. coerce is using unsafeCoerce a. So, please, please do not provide the undefined as the proof. Using this function instead of pattern-matching on equality proof, you can reduce the overhead introduced by run-time proof.

coerce' :: (a :=: b) -> a -> b

Coercion for identity types.

Re-exported modules

module Data.Singletons

module Data.Proxy