Proof.Equational

Contents

• Conversion between equalities
• Coercion
• Re-exported modules

Synopsis

• data a :~: b :: k -> k -> * where
  • Refl :: (:~:) k b b
• type (:=:) = (:~:)
• sym :: (:~:) k a b -> (:~:) k b a
• trans :: (:~:) k a b -> (:~:) k b c -> (:~:) k a c
• class Preorder eq => Equality eq where
  • symmetry :: eq a b -> eq b a
• class Preorder eq where
  • 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
• type (:/\:) a b = (a, b)
• (=<=) :: Preorder r => r x y -> Reason r y z -> r x z
• (=>=) :: Preorder r => r y z -> Reason r x y -> r x z
• (=~=) :: Preorder r => r x y -> Sing y -> r x y
• data Leibniz a b = Leibniz {
  • apply :: forall f. f a -> f b
  }
• data Reason eq x y where
  • Because :: Sing y -> eq x y -> Reason eq x y
• because :: Sing y -> eq x y -> Reason eq x y
• by :: Sing y -> eq x y -> Reason eq x y
• (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
• start :: Preorder eq => Sing a -> eq a a
• byDefinition :: (SingI a, Preorder eq) => eq a a
• admitted :: Reason eq x y
• data Proxy t :: k -> * = Proxy
• 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
  • type OriginalProp f n :: *
  • unWrap :: f n -> OriginalProp f n
  • wrap :: OriginalProp f n -> f n
• type family xs :~> a :: *
• class FromBool c where
  • type Predicate c :: Bool
  • type Args c :: [*]
  • fromBool :: (Predicate c ~ True) => Args c :~> c
• 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
• coerce :: (a :=: b) -> f a -> f b
• coerce' :: (a :=: b) -> a -> b
• module Data.Singletons
• module Data.Proxy

Documentation

Conversion between equalities

Coercion

Re-exported modules