equational-reasoning-0.2.0.7: Proof assistant for Haskell using DataKinds & PolyKinds

Safe HaskellNone
LanguageHaskell98

Proof.Equational

Contents

Synopsis

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 b b 

Instances

Equality k ((:=:) k) Source 
Preorder k ((:=:) k) Source 
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 Source

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 Source

Methods

symmetry :: eq a b -> eq b a Source

Instances

class Preorder eq where Source

Methods

reflexivity :: Sing a -> eq a a Source

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

Instances

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

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

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

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

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

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

data Leibniz a b Source

Constructors

Leibniz 

Fields

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

Instances

data Reason eq x y where Source

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 Source

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

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

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

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

admitted :: Reason eq x y Source

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 *) 
Foldable (Proxy *) 
Traversable (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 k 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 Source

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

class Proposition f where Source

Associated Types

type OriginalProp f n :: * Source

Methods

unWrap :: f n -> OriginalProp f n Source

wrap :: OriginalProp f n -> f n Source

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

Instances

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

class FromBool c where Source

Associated Types

type Predicate c :: Bool Source

type Args c :: [*] Source

Methods

fromBool :: (Predicate c ~ True) => Args c :~> c Source

Conversion between equalities

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

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

Coercion

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

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 Source

Coercion for identity types.

Re-exported modules

module Data.Proxy