equational-reasoning 0.0.3.0 → 0.0.4.0

raw patch · 2 files changed

+9/−6 lines, 2 files

Files

• Proof/Equational.hs +8/−5
• equational-reasoning.cabal +1/−1

@@ -2,7 +2,7 @@ {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies     #-} {-# LANGUAGE TypeOperators, TypeSynonymInstances                       #-} module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity'-                        ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..)+                        ,(:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)                         , Reason(..), because, by, (===), start, byDefinition                         , admitted, Proxy(..), cong, cong'                         , Proposition(..), (:~>), FromBool (..)@@ -83,15 +83,18 @@ because = Because by      = Because -infixl 4 ===, =>=, =~=+infixl 4 ===, =<=, =~=, =>= infix 5 `Because` infix 5 `because` -(=>=) :: Preorder r => r x y -> Reason r y z -> r x z-eq =>= (_ `Because` eq') = transitivity eq eq'+(=<=) :: Preorder r => r x y -> Reason r y z -> r x z+eq =<= (_ `Because` eq') = transitivity eq eq' +(=>=) :: Preorder r => r y z -> Reason r x y -> r x z+eq =>= (_ `Because` eq') = transitivity eq' eq+ (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z-(===) = (=>=)+(===) = (=<=)  (=~=) :: Preorder r => r x y -> Sing y -> r x y eq =~= _ = eq

@@ -2,7 +2,7 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.0.3.0+version:             0.0.4.0 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds -- description:          license:             BSD3