Proof.Equational

Documentation

data a :~: b :: 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 a1 a1

Instances

Equality k ((:=:) k)

Preorder k ((:=:) k)

TestEquality k ((:~:) k a)

(~) 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 (:=:) = (:~:) 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

Methods

symmetry :: eq a b -> eq b a

Instances

Equality k (Leibniz k)

Equality k ((:=:) k)

class Preorder eq where

Methods

reflexivity :: Sing a -> eq a a

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

Instances

Preorder * (->)

Preorder k (Leibniz k)

Preorder k ((:=:) k)

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)

Preorder k (Leibniz k)

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 t :: k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Functor (Proxy *)

Applicative (Proxy *)

Bounded (Proxy k s)

Enum (Proxy k s)

Eq (Proxy k s)

Ord (Proxy k s)

Read (Proxy k s)

Show (Proxy k s)

Ix (Proxy k s)

Generic (Proxy * t)

Monoid (Proxy * s)

type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy 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

Associated Types

type OriginalProp f n :: *

Methods

unWrap :: f n -> OriginalProp f n

wrap :: OriginalProp f n -> f n

type family xs :~> a :: * infixr 1

Instances

type ([] *) :~> a = a

type ((:) * x xs) :~> a = x -> (:~>) xs a

class FromBool c where

Associated Types

type Predicate c :: Bool

type Args c :: [*]

Methods

fromBool :: (Predicate c ~ True) => 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