Safe Haskell	Safe
Language	Haskell2010

Math.Tools

Synopsis

class (Category ar, Category ar') => ArrowTransformation ar ar' where
- mapA :: ar a b -> ar' a b
class (Category arr, Monoid m) => MonoidArrow arr m a where
- monoidA :: m -> arr a a
class Category arr => MonoidalCategory (arr :: k -> k -> *) where
- type Prod (arr :: k -> k -> *) (a :: k) (b :: k) :: k
- type MUnit (arr :: k -> k -> *) :: k
- (-*-) :: arr a b -> arr a' b' -> arr (Prod arr a a') (Prod arr b b')
- monoidal_assoc :: arr (Prod arr (Prod arr a b) c) (Prod arr a (Prod arr b c))
- monoidal_deassoc :: arr (Prod arr a (Prod arr b c)) (Prod arr (Prod arr a b) c)
- leftunitor :: arr (Prod arr (MUnit arr) a) a
- unleftunitor :: arr a (Prod arr (MUnit arr) a)
- rightunitor :: arr (Prod arr a (MUnit arr)) a
- unrightunitor :: arr a (Prod arr a (MUnit arr))
class MonoidalCategory arr => BraidedCategory (arr :: k -> k -> *) where
- braiding :: arr (Prod arr a b) (Prod arr b a)
class Category c => OverCategory c y where
- overmap :: c a b -> c b y -> c a y
class (Category arr, Category arr') => OppositeCategoryAction arr arr' where
- categoryA :: arr a' a -> arr' x a -> arr' x a'
class Category arr => FailureArrow arr err where
- failA :: arr err b
- catchA :: arr a b -> arr err b -> arr a b
class Category arr => Groupoid arr where
- invertA :: arr a b -> arr b a
class (Category arr, Category arr') => OpArrow p arr arr' where
- inverse_imageA :: arr a b -> arr' (p b) (p a)
class Category arr => CoArrow arr where
- coarr :: (b -> a) -> arr a b
- coleft :: arr a b -> arr (Either a d) (Either b d)
- coright :: arr a b -> arr (Either d a) (Either d b)
class Category arr => BiArrow arr where
- (<->) :: (a -> b) -> (b -> a) -> arr a b
class (Category arr, Category m) => MonoidCategory arr m f | f -> m arr where
- monoidArr :: m a a -> arr (f a) (f a)
class (BiArrow arr, FunctorArrow f arr arr) => ApplicativeBiArrow arr f where
- bipure :: arr a (f a)
- bimap :: arr (f (arr a b), f a) (f b)
- biliftA2 :: arr a (arr b c) -> arr (f a, f b) (f c)
class Category arr => CPSArrow arr where
- callcc :: (forall bot. arr c bot -> arr b c) -> arr b c
class (Category arr, Category arr') => FunctorArrow f arr arr' | f arr' -> arr, f arr -> arr' where
- amap :: arr c d -> arr' (f c) (f d)
class (FunctorArrow f arr arr, Category arr) => ApplicativeArrow f arr where
- apure :: arr a (f a)
- aapply :: f (arr a b) -> arr (f a) (f b)
alift2 :: (ApplicativeArrow f arr, ArrowApply arr) => f (arr a (arr b c)) -> arr (f a, f b) (f c)
class (Category arr, Category arr') => CoFunctorArrow f arr arr' where
- inverseImage :: arr c d -> arr' (f d) (f c)
(|>) :: CoFunctorArrow f (->) (->) => f d -> (c -> d) -> f c
class (Category arr, Category arr') => AdjunctionArrow arr arr' f g | f -> g, g -> f, arr -> arr', arr' -> arr where
- ladA :: arr (f a) b -> arr' a (g b)
- radA :: arr' a (g b) -> arr (f a) b
- unitA :: arr' a (g (f a))
- counitA :: arr (f (g b)) b
outerA :: (Arrow arr2, FunctorArrow f arr arr', FunctorArrow g arr2 arr, ArrowApply arr, ArrowApply arr') => arr2 (a, b) c -> arr' (f a, g b) (f (g c))
class FunctorArrow f arr arr => InitialAlgebraA arr a f | a -> f where
- deconstructA :: arr a (f a)
class Category a => LoopArrow a prod where
- loop_secondSA :: a (prod b d) (prod c d) -> a b c
- loop_firstSA :: a (prod d b) (prod d c) -> a b c
class Category a => MessagingArrow a where
- splitA :: a (Either b c) (Either d e) -> (a b d, a c e)
class Category a => UnifyingArrow a where
- joinA :: a (Either b b) b
class Category a => DoublingArrow a where
- doubleA :: a b (b, b)
class Category a => CircuitArrow a where
- delayA :: b -> a b b
class Category a => StorageArrow a where
- storageA :: a b c -> (a b (), a () c)
class Category a => ArrowUnit a where
- aunit :: a b ()
class Category a => ArrowFix a prod where
- fixArrow :: a (prod b c) c -> a b c
class Category a => ArrowCircuit a where
- delay :: b -> a b b
class Category a => ArrowDual a d where
- collapseArrow :: d (d a) b c -> a b c
class ArrowDual a d => RecArrow a d where
- recArrow :: a b c -> d a b c
class ArrowDual a d => ArrowDualApp a d where
- appArrow :: a (a b c, d a b c) c
module Math.Tools.Adjunction
module Math.Tools.CoFunctor
module Math.Tools.CoMonad
module Math.Tools.Complex
module Math.Tools.Expression
class BiFunctor op
class Functor f => InterleaveFunctor f where
- interleave :: f a -> f a -> f a
(<&>) :: Applicative f => f a -> f b -> f (a, b)
unzipWith :: Functor f => (a -> (b, c)) -> f a -> (f b, f c)
fst3 :: (a, b, c) -> a
snd3 :: (a, b, c) -> b
funzip :: Functor f => f (a, b) -> (f a, f b)
thrd3 :: (a, b, c) -> c
funzip3 :: Functor f => f (a, b, c) -> (f a, f b, f c)
fzipWith3 :: Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
fzip :: Applicative f => f a -> f b -> f (a, b)
fzip3 :: Applicative f => f a -> f b -> f c -> f (a, b, c)
fzip4 :: Applicative f => f a -> f b -> f c -> f d -> f (a, b, c, d)
liftA4 :: Applicative f => (a -> b -> c -> d -> e) -> f a -> f b -> f c -> f d -> f e
module Math.Tools.Identity
module Math.Tools.Id
module Math.Tools.I
module Math.Tools.Integer
module Math.Tools.Integer
module Math.Tools.Isomorphism
module Math.Tools.LineInfo
module Math.Tools.List
module Math.Tools.Map
module Math.Tools.Map
module Math.Tools.Maybe
module Math.Tools.Median
module Math.Tools.Monad
module Math.Tools.Monoid
module Math.Tools.NaturalNumber
module Math.Tools.NaturalTransformation
module Math.Tools.Orthogonal
module Math.Tools.ParseMonad
module Math.Tools.ParserInterface
module Math.Tools.Parser
module Math.Tools.ParsingCombinators
module Math.Tools.PrettyP
newtype Prop a = Characteristic {
- runCharacteristic :: a -> Bool
}
subseteq :: Universe a => Prop a -> Prop a -> Bool
intersects :: Universe a => Prop a -> Prop a -> Bool
split_prop :: Universe a => Prop a -> ([a], [a])
propositional_table :: Universe a => Prop a -> [(a, Bool)]
fromBool :: Bool -> Prop a
prop_substitute :: Contravariant p => p a -> p (a, b)
prop_exists :: (Adjunction f p, Contravariant p) => f (p a) -> (a, b)
prop_exists_snd :: (Adjunction f p, Contravariant p) => f (p b) -> (a, b)
prop_always :: (Adjunction p g, Contravariant p) => a -> g (p (a, b))
prop_always_snd :: (Adjunction p g, Contravariant p) => b -> g (p (a, b))
axiom_N :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
axiom_K :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
axiom_4 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
axiom_B :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
axiom_D :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
axiom_5 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
axiom_T :: (ModalLogic p, ImplicativeLogic p) => p a -> p a
system_K :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
system_T :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
system_S4 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
system_S5 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
system_D :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a
vector_equalizer :: (Eq (n a), LinearTransform m n a) => (m :*: n) a -> (m :*: n) a -> Prop (m a)
list_truthvalues :: Universe a => Prop a -> [(a, Bool)]
apply :: Prop (Prop b, b)
result :: Eq a => a -> Prop a
existential_bind :: Universe a => Prop a -> (a -> Prop b) -> Prop b
existential_join :: (Universe b, Eq b) => Prop (Prop b) -> Prop b
universal_bind :: Universe a => Prop a -> (a -> Prop b) -> Prop b
universal_join :: (Universe b, Eq b) => Prop (Prop b) -> Prop b
prop_fixedpoint :: (Prop a -> Prop a) -> Prop a
truthvalue :: Bool -> Prop a
satisfiable :: Universe a => Prop a -> Bool
axiom :: Universe a => Prop a -> Bool
notMember :: a -> Prop a -> Bool
subseteq_prop :: Prop a -> Prop a -> Prop a
is_section :: Prop a -> (Bool -> a) -> Bool
doublePropJoin :: Prop (Prop (Prop (Prop a))) -> Prop (Prop a)
fromAssoc :: Eq a => [(a, Bool)] -> Prop a
fromAssocWith :: Eq a => [(a, b)] -> Prop b -> Prop a
prop_fromList :: Eq a => [a] -> Prop a
prop_fromSet :: Ord a => Set a -> Prop a
prop_fromMap :: (Ord i, Eq e) => Map i e -> Prop (i, e)
map_prop :: (Eq b, Universe a) => (a -> b) -> Prop a -> Prop b
equalizer_fixedpoint :: HasEqualizers p a => (a -> a) -> p a
invertible :: HasEqualizers p a => (b -> a) -> (a -> b) -> p a
kernel :: (Num c, HasEqualizers p c) => (a -> c) -> p a
ternary_op :: (Bool -> Bool -> Bool -> Bool) -> Prop a -> Prop a -> Prop a -> Prop a
binary_op :: (Bool -> Bool -> Bool) -> Prop a -> Prop a -> Prop a
gen_binary_op :: (b -> b' -> c) -> (a -> b) -> (a -> b') -> a -> c
binary :: Relational p => (a -> b -> p c) -> p (a, (b, c))
evaluate :: a -> Prop (Prop a)
evaluate' :: (Universe a, Eq a) => a -> Prop (Prop a)
integrate_prop :: Universe a => Prop a -> Prop (Prop a)
intersect :: Prop a -> Prop a -> Prop a
intersect3 :: Prop a -> Prop a -> Prop a -> Prop a
median3 :: Prop a -> Prop a -> Prop a -> Prop a
union :: Prop a -> Prop a -> Prop a
union3 :: Prop a -> Prop a -> Prop a -> Prop a
excluded_middle :: Universe b => Prop b -> Bool
noncontradiction :: Universe b => Prop b -> Bool
demorgan_union :: Universe a => Prop a -> Prop a -> Bool
demorgan_intersect :: Universe a => Prop a -> Prop a -> Bool
disjunction_commutative :: Universe a => Prop a -> Prop a -> Bool
conjunction_commutative :: Universe a => Prop a -> Prop a -> Bool
graph :: Eq b => (a -> b) -> Prop (a, b)
image_factorization :: (Eq b, Universe a) => (a -> b) -> Prop b
bind :: Universe b => (a -> Prop b) -> (b -> Prop c) -> a -> Prop c
prop_compose :: Universe b => Prop (a, b) -> Prop (b, c) -> Prop (a, c)
transitive :: Universe a => Prop (a, a) -> Bool
antisymmetric :: Eq a => Prop (a, a) -> Prop (a, a)
prop_iso_terminal :: Prop ((), b) -> Prop b
prop_iso_terminal_inverse :: Prop b -> Prop ((), b)
fiber :: HasEqualizers Prop c => (b -> c) -> c -> Prop b
fiber_ :: Eq b => (a -> b) -> b -> Prop a
equivalence_relation :: HasEqualizers Prop b => (a -> b) -> Prop (a, a)
reflexive :: Eq a => Prop (a, a)
reflexive_closure :: Eq a => Prop (a, a) -> Prop (a, a)
symmetric_closure :: Prop (a, a) -> Prop (a, a)
transitive_step :: Universe a => Prop (a, a) -> Prop (a, a)
transitive_closure :: Universe a => Prop (a, a) -> Prop (a, a)
equivalence_generated_by :: (Eq a, Universe a) => Prop (a, a) -> Prop (a, a)
opposite :: Prop (a, b) -> Prop (b, a)
leftAdjunct_prop :: (a -> Prop b) -> b -> Prop a
unit_prop :: b -> Prop (Prop b)
rel_prop :: (a -> Bool) -> Prop a
binary_rel_prop :: (a -> a -> Bool) -> Prop (a, a)
binary_rel :: (a -> a -> Bool) -> a -> Prop a
equal_functions :: (Universe a, Eq b) => Prop (a -> b, a -> b)
test_equality_at :: a -> Prop (Prop a, Prop a)
equalizer_prop :: Prop a -> Prop a -> Prop a
pullback_prop :: Prop a -> Prop b -> Prop (a, b)
sum :: Prop a -> Prop b -> Prop (Either a b)
prop_and :: Prop (Either a b) -> Prop (a, b)
prop_or :: Prop (Either a b) -> Prop (a, b)
prop_if :: Prop a -> Prop (Either a a) -> Prop a
prop_if_general :: Prop a -> Prop (Either b c) -> Prop (a, b, c)
equal :: Eq a => Prop (a, a)
not_equal :: Eq a => Prop (a, a)
lessthan :: Ord a => Prop (a, a)
lesseq :: Ord a => Prop (a, a)
or_list_prop :: Prop a -> Prop [a]
and_list_prop :: Prop a -> Prop [a]
enumerate :: Universe a => Prop a -> [a]
existential_map :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b
universal_map :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b
prop_existential :: Universe b => Prop (a, b) -> Prop a
prop_universal :: Universe b => Prop (a, b) -> Prop a
image :: Universe a => Prop (a, b) -> Prop b
prop_universal_image :: (Universe a, Universe b, Eq b) => Prop (a, b) -> Prop b
forevery :: Universe b => Prop b -> Prop ()
newtype b :\: a = PSub {
- runpsub :: PProp a -> PProp b
}
data PProp a where
- PProp :: Prop a -> PProp a
- PNeg :: (Prop a -> Prop b) -> PProp (b :\: a)
pneg_func :: (a -> b) -> PProp (a :\: b)
module Math.Tools.Tree
module Math.Tools.Universe
module Math.Tools.Visitor

Documentation

class (Category ar, Category ar') => ArrowTransformation ar ar' where Source #

Methods

mapA :: ar a b -> ar' a b Source #

Instances

Instances details

Arrow arr => ArrowTransformation (:==:) (arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Isomorphism Methods mapA :: forall (a :: k) (b :: k). (a :==: b) -> arr a b Source #
Arrow ar => ArrowTransformation (->) (ar :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Arrow Methods mapA :: forall (a :: k) (b :: k). (a -> b) -> ar a b Source #

class (Category arr, Monoid m) => MonoidArrow arr m a where Source #

Methods

monoidA :: m -> arr a a Source #

Instances

Instances details

Arrow arr => MonoidArrow (arr :: Type -> Type -> Type) (Three Bool Bool) Bool Source #
Instance details Defined in Math.Graph.GraphMonoid Methods monoidA :: Three Bool Bool -> arr Bool Bool Source #
Monoid (m Bool Bool) => MonoidArrow (InGraphA m a :: Type -> Type -> Type) (m Bool Bool) (a :: Type) Source #
Instance details Defined in Math.Graph.InGraphA Methods monoidA :: m Bool Bool -> InGraphA m a a a Source #
MonoidArrow (->) (Four Bool Bool) Bool Source #
Instance details Defined in Math.Graph.GraphMonoid Methods monoidA :: Four Bool Bool -> Bool -> Bool Source #

class Category arr => MonoidalCategory (arr :: k -> k -> *) where Source #

https://en.wikipedia.org/wiki/Monoidal_category

Associated Types

type Prod (arr :: k -> k -> *) (a :: k) (b :: k) :: k Source #

type MUnit (arr :: k -> k -> *) :: k Source #

Methods

(-*-) :: arr a b -> arr a' b' -> arr (Prod arr a a') (Prod arr b b') Source #

monoidal_assoc :: arr (Prod arr (Prod arr a b) c) (Prod arr a (Prod arr b c)) Source #

monoidal_deassoc :: arr (Prod arr a (Prod arr b c)) (Prod arr (Prod arr a b) c) Source #

leftunitor :: arr (Prod arr (MUnit arr) a) a Source #

unleftunitor :: arr a (Prod arr (MUnit arr) a) Source #

rightunitor :: arr (Prod arr a (MUnit arr)) a Source #

unrightunitor :: arr a (Prod arr a (MUnit arr)) Source #

Instances

Instances details

MonoidalCategory (->) Source #

https://en.wikipedia.org/wiki/Monoidal_category

Instance details

Defined in Math.Tools.Arrow

Associated Types

type Prod (->) a b :: k Source #

type MUnit (->) :: k Source #

Methods

(-*-) :: forall (a :: k) (b :: k) (a' :: k) (b' :: k). (a -> b) -> (a' -> b') -> Prod (->) a a' -> Prod (->) b b' Source #

monoidal_assoc :: forall (a :: k) (b :: k) (c :: k). Prod (->) (Prod (->) a b) c -> Prod (->) a (Prod (->) b c) Source #

monoidal_deassoc :: forall (a :: k) (b :: k) (c :: k). Prod (->) a (Prod (->) b c) -> Prod (->) (Prod (->) a b) c Source #

leftunitor :: forall (a :: k). Prod (->) (MUnit (->)) a -> a Source #

unleftunitor :: forall (a :: k). a -> Prod (->) (MUnit (->)) a Source #

rightunitor :: forall (a :: k). Prod (->) a (MUnit (->)) -> a Source #

unrightunitor :: forall (a :: k). a -> Prod (->) a (MUnit (->)) Source #

class MonoidalCategory arr => BraidedCategory (arr :: k -> k -> *) where Source #

Methods

braiding :: arr (Prod arr a b) (Prod arr b a) Source #

Instances

Instances details

BraidedCategory (->) Source #
Instance details Defined in Math.Tools.Arrow Methods braiding :: forall (a :: k) (b :: k). Prod (->) a b -> Prod (->) b a Source #

class Category c => OverCategory c y where Source #

Methods

overmap :: c a b -> c b y -> c a y Source #

Instances

Instances details

OverCategory (->) (a :: Type) Source #
Instance details Defined in Math.Tools.Prop Methods overmap :: forall (a0 :: k) (b :: k). (a0 -> b) -> (b -> a) -> a0 -> a Source #

class (Category arr, Category arr') => OppositeCategoryAction arr arr' where Source #

Methods

categoryA :: arr a' a -> arr' x a -> arr' x a' Source #

class Category arr => FailureArrow arr err where Source #

Methods

failA :: arr err b Source #

catchA :: arr a b -> arr err b -> arr a b Source #

Instances

Instances details

FailureArrow (Kleisli IO) IOError Source #
Instance details Defined in Math.Tools.Arrow Methods failA :: forall (b :: k). Kleisli IO IOError b Source # catchA :: forall (a :: k) (b :: k). Kleisli IO a b -> Kleisli IO IOError b -> Kleisli IO a b Source #
FailureArrow (Kleisli IO) Doc Source #
Instance details Defined in Math.Tools.Arrow Methods failA :: forall (b :: k). Kleisli IO Doc b Source # catchA :: forall (a :: k) (b :: k). Kleisli IO a b -> Kleisli IO Doc b -> Kleisli IO a b Source #
FailureArrow (Kleisli IO) [Doc] Source #
Instance details Defined in Math.Tools.Arrow Methods failA :: forall (b :: k). Kleisli IO [Doc] b Source # catchA :: forall (a :: k) (b :: k). Kleisli IO a b -> Kleisli IO [Doc] b -> Kleisli IO a b Source #

class Category arr => Groupoid arr where Source #

Methods

invertA :: arr a b -> arr b a Source #

Instances

Instances details

Groupoid (:==:) Source #
Instance details Defined in Math.Tools.Isomorphism Methods invertA :: forall (a :: k) (b :: k). (a :==: b) -> b :==: a Source #
Groupoid ParsingA Source #
Instance details Defined in Math.Tools.ParsingCombinators Methods invertA :: forall (a :: k) (b :: k). ParsingA a b -> ParsingA b a Source #
FunctorArrow v (->) (->) => Groupoid (IsoA (NumExpr v) :: Type -> Type -> Type) Source #
Instance details Defined in Math.Number.NumericExpression Methods invertA :: forall (a :: k) (b :: k). IsoA (NumExpr v) a b -> IsoA (NumExpr v) b a Source #
Groupoid (IsoA Var) Source #
Instance details Defined in Math.Number.NumericExpression Methods invertA :: forall (a :: k) (b :: k). IsoA Var a b -> IsoA Var b a Source #
FunctorArrow v (->) (->) => Groupoid (IsoA (VectorSpaceExpr v) :: Type -> Type -> Type) Source #
Instance details Defined in Math.Number.NumericExpression Methods invertA :: forall (a :: k) (b :: k). IsoA (VectorSpaceExpr v) a b -> IsoA (VectorSpaceExpr v) b a Source #
Category arr => Groupoid (GroupT arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Monoid Methods invertA :: forall (a :: k) (b :: k). GroupT arr a b -> GroupT arr b a Source #
Category arr => Groupoid (IsomorphismA arr :: k -> k -> Type) Source #
Instance details Defined in Math.Tools.Isomorphism Methods invertA :: forall (a :: k0) (b :: k0). IsomorphismA arr a b -> IsomorphismA arr b a Source #

class (Category arr, Category arr') => OpArrow p arr arr' where Source #

Methods

inverse_imageA :: arr a b -> arr' (p b) (p a) Source #

class Category arr => CoArrow arr where Source #

Methods

coarr :: (b -> a) -> arr a b Source #

coleft :: arr a b -> arr (Either a d) (Either b d) Source #

coright :: arr a b -> arr (Either d a) (Either d b) Source #

class Category arr => BiArrow arr where Source #

Methods

(<->) :: (a -> b) -> (b -> a) -> arr a b Source #

Instances

Instances details

BiArrow (:==:) Source #
Instance details Defined in Math.Tools.Isomorphism Methods (<->) :: (a -> b) -> (b -> a) -> a :==: b Source #
BiArrow ParsingA Source #
Instance details Defined in Math.Tools.ParsingCombinators Methods (<->) :: (a -> b) -> (b -> a) -> ParsingA a b Source #
FunctorArrow v (->) (->) => BiArrow (IsoA (NumExpr v)) Source #
Instance details Defined in Math.Number.NumericExpression Methods (<->) :: (a -> b) -> (b -> a) -> IsoA (NumExpr v) a b Source #
BiArrow (IsoA Var) Source #
Instance details Defined in Math.Number.NumericExpression Methods (<->) :: (a -> b) -> (b -> a) -> IsoA Var a b Source #
FunctorArrow v (->) (->) => BiArrow (IsoA (VectorSpaceExpr v)) Source #
Instance details Defined in Math.Number.NumericExpression Methods (<->) :: (a -> b) -> (b -> a) -> IsoA (VectorSpaceExpr v) a b Source #
Arrow arr => BiArrow (IsomorphismA arr) Source #
Instance details Defined in Math.Tools.Isomorphism Methods (<->) :: (a -> b) -> (b -> a) -> IsomorphismA arr a b Source #

class (Category arr, Category m) => MonoidCategory arr m f | f -> m arr where Source #

Methods

monoidArr :: m a a -> arr (f a) (f a) Source #

class (BiArrow arr, FunctorArrow f arr arr) => ApplicativeBiArrow arr f where Source #

Minimal complete definition

bipure, biliftA2

Methods

bipure :: arr a (f a) Source #

bimap :: arr (f (arr a b), f a) (f b) Source #

biliftA2 :: arr a (arr b c) -> arr (f a, f b) (f c) Source #

class Category arr => CPSArrow arr where Source #

Methods

callcc :: (forall bot. arr c bot -> arr b c) -> arr b c Source #

class (Category arr, Category arr') => FunctorArrow f arr arr' | f arr' -> arr, f arr -> arr' where Source #

Arrow version of Functor from Haskell Prelude

Methods

amap :: arr c d -> arr' (f c) (f d) Source #

Instances

Instances details

FunctorArrow Endo (:==:) (:==:) Source #
Instance details Defined in Math.Graph.GraphMonoid Methods amap :: forall (c :: k) (d :: k). (c :==: d) -> Endo c :==: Endo d Source #
FunctorArrow Vector2 (:==:) (:==:) Source #
Instance details Defined in Math.Matrix.Vector2 Methods amap :: forall (c :: k) (d :: k). (c :==: d) -> Vector2 c :==: Vector2 d Source #
FunctorArrow I (:==:) (:==:) Source #
Instance details Defined in Math.Tools.Isomorphism Methods amap :: forall (c :: k) (d :: k). (c :==: d) -> I c :==: I d Source #
ArrowChoice ar => FunctorArrow Queue (ar :: Type -> Type -> Type) (ar :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Queue Methods amap :: forall (c :: k) (d :: k). ar c d -> ar (Queue c) (Queue d) Source #
ArrowChoice arr => FunctorArrow Maybe (arr :: Type -> Type -> Type) (arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Arrow Methods amap :: forall (c :: k) (d :: k). arr c d -> arr (Maybe c) (Maybe d) Source #
ArrowChoice arr => FunctorArrow List (arr :: Type -> Type -> Type) (arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Arrow Methods amap :: forall (c :: k) (d :: k). arr c d -> arr [c] [d] Source #
FunctorArrow Vector1 (->) (->) Source #
Instance details Defined in Math.Matrix.Vector1 Methods amap :: forall (c :: k) (d :: k). (c -> d) -> Vector1 c -> Vector1 d Source #
FunctorArrow Var (->) (->) Source #
Instance details Defined in Math.Number.NumericExpression Methods amap :: forall (c :: k) (d :: k). (c -> d) -> Var c -> Var d Source #
FunctorArrow I (->) (->) Source #
Instance details Defined in Math.Tools.Arrow Methods amap :: forall (c :: k) (d :: k). (c -> d) -> I c -> I d Source #
ArrowChoice arr => FunctorArrow (Either b :: Type -> Type) (arr :: Type -> Type -> Type) (arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Arrow Methods amap :: forall (c :: k) (d :: k). arr c d -> arr (Either b c) (Either b d) Source #
(Ord i, ArrowChoice arr) => FunctorArrow (Map i :: Type -> Type) (arr :: Type -> Type -> Type) (arr :: Type -> Type -> Type) Source #
Instance details Defined in Math.Tools.Map Methods amap :: forall (c :: k) (d :: k). arr c d -> arr (Map i c) (Map i d) Source #
FunctorArrow v (->) (->) => FunctorArrow (NumExpr v :: Type -> Type) (->) (->) Source #
Instance details Defined in Math.Number.NumericExpression Methods amap :: forall (c :: k) (d :: k). (c -> d) -> NumExpr v c -> NumExpr v d Source #
FunctorArrow v (->) (->) => FunctorArrow (VectorSpaceExpr v :: Type -> Type) (->) (->) Source #
Instance details Defined in Math.Number.NumericExpression Methods amap :: forall (c :: k) (d :: k). (c -> d) -> VectorSpaceExpr v c -> VectorSpaceExpr v d Source #

class (FunctorArrow f arr arr, Category arr) => ApplicativeArrow f arr where Source #

Arrow version of Applicative from Haskell Prelude

Methods

apure :: arr a (f a) Source #

aapply :: f (arr a b) -> arr (f a) (f b) Source #

alift2 :: (ApplicativeArrow f arr, ArrowApply arr) => f (arr a (arr b c)) -> arr (f a, f b) (f c) Source #

class (Category arr, Category arr') => CoFunctorArrow f arr arr' where Source #

Methods

inverseImage :: arr c d -> arr' (f d) (f c) Source #

(|>) :: CoFunctorArrow f (->) (->) => f d -> (c -> d) -> f c Source #

class (Category arr, Category arr') => AdjunctionArrow arr arr' f g | f -> g, g -> f, arr -> arr', arr' -> arr where Source #

Minimal complete definition

ladA, radA

Methods

ladA :: arr (f a) b -> arr' a (g b) Source #

radA :: arr' a (g b) -> arr (f a) b Source #

unitA :: arr' a (g (f a)) Source #

counitA :: arr (f (g b)) b Source #

outerA :: (Arrow arr2, FunctorArrow f arr arr', FunctorArrow g arr2 arr, ArrowApply arr, ArrowApply arr') => arr2 (a, b) c -> arr' (f a, g b) (f (g c)) Source #

class FunctorArrow f arr arr => InitialAlgebraA arr a f | a -> f where Source #

Methods

deconstructA :: arr a (f a) Source #

class Category a => LoopArrow a prod where Source #

Methods

loop_secondSA :: a (prod b d) (prod c d) -> a b c Source #

loop_firstSA :: a (prod d b) (prod d c) -> a b c Source #

class Category a => MessagingArrow a where Source #

Methods

splitA :: a (Either b c) (Either d e) -> (a b d, a c e) Source #

class Category a => UnifyingArrow a where Source #

Methods

joinA :: a (Either b b) b Source #

class Category a => DoublingArrow a where Source #

Methods

doubleA :: a b (b, b) Source #

class Category a => CircuitArrow a where Source #

Methods

delayA :: b -> a b b Source #

class Category a => StorageArrow a where Source #

Methods

storageA :: a b c -> (a b (), a () c) Source #

class Category a => ArrowUnit a where Source #

Methods

aunit :: a b () Source #

class Category a => ArrowFix a prod where Source #

Methods

fixArrow :: a (prod b c) c -> a b c Source #

class Category a => ArrowCircuit a where Source #

Methods

delay :: b -> a b b Source #

class Category a => ArrowDual a d where Source #

Methods

collapseArrow :: d (d a) b c -> a b c Source #

class ArrowDual a d => RecArrow a d where Source #

Methods

recArrow :: a b c -> d a b c Source #

class ArrowDual a d => ArrowDualApp a d where Source #

Methods

appArrow :: a (a b c, d a b c) c Source #

module Math.Tools.Adjunction

module Math.Tools.CoFunctor

module Math.Tools.CoMonad

module Math.Tools.Complex

module Math.Tools.Expression

class BiFunctor op Source #

Minimal complete definition

bimap

class Functor f => InterleaveFunctor f where Source #

Methods

interleave :: f a -> f a -> f a infixr 8 Source #

Instances

Instances details

InterleaveFunctor Stream Source #
Instance details Defined in Math.Number.Stream Methods interleave :: Stream a -> Stream a -> Stream a Source #
InterleaveFunctor Queue Source #
Instance details Defined in Math.Tools.Queue Methods interleave :: Queue a -> Queue a -> Queue a Source #
InterleaveFunctor List Source #
Instance details Defined in Math.Tools.List Methods interleave :: [a] -> [a] -> [a] Source #

(<&>) :: Applicative f => f a -> f b -> f (a, b) infixl 8 Source #

unzipWith :: Functor f => (a -> (b, c)) -> f a -> (f b, f c) Source #

fst3 :: (a, b, c) -> a Source #

snd3 :: (a, b, c) -> b Source #

funzip :: Functor f => f (a, b) -> (f a, f b) Source #

thrd3 :: (a, b, c) -> c Source #

funzip3 :: Functor f => f (a, b, c) -> (f a, f b, f c) Source #

fzipWith3 :: Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d Source #

fzip :: Applicative f => f a -> f b -> f (a, b) Source #

fzip3 :: Applicative f => f a -> f b -> f c -> f (a, b, c) Source #

fzip4 :: Applicative f => f a -> f b -> f c -> f d -> f (a, b, c, d) Source #

liftA4 :: Applicative f => (a -> b -> c -> d -> e) -> f a -> f b -> f c -> f d -> f e Source #

module Math.Tools.Identity

module Math.Tools.Id

module Math.Tools.I

module Math.Tools.Integer

module Math.Tools.Isomorphism

module Math.Tools.LineInfo

module Math.Tools.List

module Math.Tools.Map

module Math.Tools.Maybe

module Math.Tools.Median

module Math.Tools.Monad

module Math.Tools.Monoid

module Math.Tools.NaturalNumber

module Math.Tools.NaturalTransformation

module Math.Tools.Orthogonal

module Math.Tools.ParseMonad

module Math.Tools.ParserInterface

module Math.Tools.Parser

module Math.Tools.ParsingCombinators

module Math.Tools.PrettyP

newtype Prop a Source #

We must represent classical logic with characteristic functions, because of the excluded middle axiom, and because characteristic functions (as properties) have complex relationship with possible elements of a. See the Universe type class for a solution. For exposition of classical logic used here, see "Lawvere,Rosebrugh: Sets for mathematics".

Constructors

Characteristic
Fields runCharacteristic :: a -> Bool

Instances

Instances details

Contravariant Prop Source #
Instance details Defined in Math.Tools.Prop Methods contramap :: (a' -> a) -> Prop a -> Prop a' # (>$) :: b -> Prop b -> Prop a #
BinaryLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods toBool :: Prop () -> Bool Source #
BooleanLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods true :: Prop a Source #
Existential Prop Source #
Instance details Defined in Math.Tools.Prop Methods direct_image :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source # universal_image :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source #
ImplicativeLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-=>-) :: Prop a -> Prop a -> Prop a Source #
Propositional Prop Source #
Instance details Defined in Math.Tools.Prop Methods runProposition :: Prop a -> a -> Prop () Source #
PropositionalLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-&-) :: Prop a -> Prop a -> Prop a Source # (-\|-) :: Prop a -> Prop a -> Prop a Source # invert :: Prop a -> Prop a Source #
Relational Prop Source #	relation and unrelation represent the natural isomorphism \[Hom(-,P(A)) \cong Sub(- \times A)\]
Instance details Defined in Math.Tools.Prop Methods relation :: (a -> Prop b) -> Prop (a, b) Source # unrelation :: Prop (a, b) -> a -> Prop b Source #
SubtractiveLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-\-) :: Prop a -> Prop a -> Prop a Source #
UniversalLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods singleton :: Eq a => a -> Prop a Source # all_members :: Universe a => Prop a Source #
Eq c => HasEqualizers Prop c Source #
Instance details Defined in Math.Tools.Prop Methods equalizer :: (a -> c) -> (a -> c) -> Prop a Source # pullback :: (a -> c) -> (b -> c) -> Prop (a, b) Source #
(Show a, Universe a) => Show (Prop a) Source #
Instance details Defined in Math.Tools.Prop Methods showsPrec :: Int -> Prop a -> ShowS # show :: Prop a -> String # showList :: [Prop a] -> ShowS #
(Universe a, Eq a) => Universe (Prop a) Source #
Instance details Defined in Math.Tools.Prop Methods all_elements :: [Prop a] Source #
Builder (Prop a) Source #
Instance details Defined in Math.Tools.Prop Associated Types data Unfold (Prop a) :: Type -> Type Source # Methods build :: Unfold (Prop a) a0 -> a0 -> Prop a Source #
Visitor (Prop a) Source #
Instance details Defined in Math.Tools.Prop Associated Types data Fold (Prop a) :: Type -> Type Source # Methods visit :: Fold (Prop a) a0 -> Prop a -> a0 Source #
Universe a => Eq (Prop a) Source #
Instance details Defined in Math.Tools.Prop Methods (==) :: Prop a -> Prop a -> Bool # (/=) :: Prop a -> Prop a -> Bool #
Universe a => Ord (Prop a) Source #
Instance details Defined in Math.Tools.Prop Methods compare :: Prop a -> Prop a -> Ordering # (<) :: Prop a -> Prop a -> Bool # (<=) :: Prop a -> Prop a -> Bool # (>) :: Prop a -> Prop a -> Bool # (>=) :: Prop a -> Prop a -> Bool # max :: Prop a -> Prop a -> Prop a # min :: Prop a -> Prop a -> Prop a #
data Fold (Prop a) b Source #
Instance details Defined in Math.Tools.Prop data Fold (Prop a) b = PropFold [a] (a -> c) (a -> c) ([c] -> b)
data Unfold (Prop a) b Source #
Instance details Defined in Math.Tools.Prop data Unfold (Prop a) b = PropUnfold (b -> a -> Bool)

subseteq :: Universe a => Prop a -> Prop a -> Bool Source #

intersects :: Universe a => Prop a -> Prop a -> Bool Source #

split_prop :: Universe a => Prop a -> ([a], [a]) Source #

See "Soare: Recursively enumerable sets and degrees", this is split of recursive into two recursively enumerable sets.

propositional_table :: Universe a => Prop a -> [(a, Bool)] Source #

fromBool :: Bool -> Prop a Source #

prop_substitute :: Contravariant p => p a -> p (a, b) Source #

prop_exists :: (Adjunction f p, Contravariant p) => f (p a) -> (a, b) Source #

prop_exists_snd :: (Adjunction f p, Contravariant p) => f (p b) -> (a, b) Source #

prop_always :: (Adjunction p g, Contravariant p) => a -> g (p (a, b)) Source #

prop_always_snd :: (Adjunction p g, Contravariant p) => b -> g (p (a, b)) Source #

axiom_N :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_K :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_4 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_B :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_D :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_5 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

axiom_T :: (ModalLogic p, ImplicativeLogic p) => p a -> p a Source #

https://en.wikipedia.org/wiki/Modal_logic

system_K :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

system_T :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

system_S4 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

system_S5 :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

system_D :: (ModalLogic p, ImplicativeLogic p) => p a -> p a -> p a Source #

vector_equalizer :: (Eq (n a), LinearTransform m n a) => (m :*: n) a -> (m :*: n) a -> Prop (m a) Source #

list_truthvalues :: Universe a => Prop a -> [(a, Bool)] Source #

It is impossible to convert characteristic index into recursively enumerable index (indexing of r.e. sets), or into canonical index (which has one bit per element describing membership). Thus we must use the Universe constraint.

apply :: Prop (Prop b, b) Source #

result :: Eq a => a -> Prop a Source #

result and the bind operations provide Monad instance, except for the | fact that the Universe and Eq constraints are required. Thus an adjunction instance also exists.

existential_bind :: Universe a => Prop a -> (a -> Prop b) -> Prop b Source #

existential_join :: (Universe b, Eq b) => Prop (Prop b) -> Prop b Source #

universal_bind :: Universe a => Prop a -> (a -> Prop b) -> Prop b Source #

universal_join :: (Universe b, Eq b) => Prop (Prop b) -> Prop b Source #

prop_fixedpoint :: (Prop a -> Prop a) -> Prop a Source #

truthvalue :: Bool -> Prop a Source #

satisfiable :: Universe a => Prop a -> Bool Source #

Satisfiable returns true if there exists an element of the universe such that the proposition is satisfied. Note symmetry with axiom.

axiom :: Universe a => Prop a -> Bool Source #

axiom returns true, if the proposition holds for all elements of the universe.

notMember :: a -> Prop a -> Bool Source #

subseteq_prop :: Prop a -> Prop a -> Prop a Source #

\[x \in subseteq i j \iff x \in i \implies x \in j\]

is_section :: Prop a -> (Bool -> a) -> Bool Source #

doublePropJoin :: Prop (Prop (Prop (Prop a))) -> Prop (Prop a) Source #

fromAssoc :: Eq a => [(a, Bool)] -> Prop a Source #

fromAssocWith :: Eq a => [(a, b)] -> Prop b -> Prop a Source #

prop_fromList :: Eq a => [a] -> Prop a Source #

prop_fromSet :: Ord a => Set a -> Prop a Source #

prop_fromMap :: (Ord i, Eq e) => Map i e -> Prop (i, e) Source #

map_prop :: (Eq b, Universe a) => (a -> b) -> Prop a -> Prop b Source #

Due to constraints, Prop cannot be made as instance of Functor.

equalizer_fixedpoint :: HasEqualizers p a => (a -> a) -> p a Source #

invertible :: HasEqualizers p a => (b -> a) -> (a -> b) -> p a Source #

kernel :: (Num c, HasEqualizers p c) => (a -> c) -> p a Source #

ternary_op :: (Bool -> Bool -> Bool -> Bool) -> Prop a -> Prop a -> Prop a -> Prop a Source #

binary_op :: (Bool -> Bool -> Bool) -> Prop a -> Prop a -> Prop a Source #

gen_binary_op :: (b -> b' -> c) -> (a -> b) -> (a -> b') -> a -> c Source #

binary :: Relational p => (a -> b -> p c) -> p (a, (b, c)) Source #

evaluate :: a -> Prop (Prop a) Source #

evaluate' :: (Universe a, Eq a) => a -> Prop (Prop a) Source #

integrate_prop :: Universe a => Prop a -> Prop (Prop a) Source #

intersect :: Prop a -> Prop a -> Prop a Source #

intersect3 :: Prop a -> Prop a -> Prop a -> Prop a Source #

median3 :: Prop a -> Prop a -> Prop a -> Prop a Source #

union :: Prop a -> Prop a -> Prop a Source #

union3 :: Prop a -> Prop a -> Prop a -> Prop a Source #

excluded_middle :: Universe b => Prop b -> Bool Source #

noncontradiction :: Universe b => Prop b -> Bool Source #

demorgan_union :: Universe a => Prop a -> Prop a -> Bool Source #

demorgan_intersect :: Universe a => Prop a -> Prop a -> Bool Source #

disjunction_commutative :: Universe a => Prop a -> Prop a -> Bool Source #

conjunction_commutative :: Universe a => Prop a -> Prop a -> Bool Source #

graph :: Eq b => (a -> b) -> Prop (a, b) Source #

\[graph(f) = [<x,y> | y = f(x)]\]

image_factorization :: (Eq b, Universe a) => (a -> b) -> Prop b Source #

bind :: Universe b => (a -> Prop b) -> (b -> Prop c) -> a -> Prop c Source #

prop_compose :: Universe b => Prop (a, b) -> Prop (b, c) -> Prop (a, c) Source #

transitive :: Universe a => Prop (a, a) -> Bool Source #

\[<x,z> \in transitive \mathbb{R} \iff (\forall y. <x,y> \in \mathbb{R} & <y,z> \in \mathbb{R} \implies <x,z> \in \mathbb{R})\]

antisymmetric :: Eq a => Prop (a, a) -> Prop (a, a) Source #

prop_iso_terminal :: Prop ((), b) -> Prop b Source #

prop_iso_terminal_inverse :: Prop b -> Prop ((), b) Source #

fiber :: HasEqualizers Prop c => (b -> c) -> c -> Prop b Source #

\[fiber(p,y) = { x | p(x) = y } = p^{-1}({y})\]

fiber_ :: Eq b => (a -> b) -> b -> Prop a Source #

equivalence_relation :: HasEqualizers Prop b => (a -> b) -> Prop (a, a) Source #

reflexive :: Eq a => Prop (a, a) Source #

reflexive_closure :: Eq a => Prop (a, a) -> Prop (a, a) Source #

symmetric_closure :: Prop (a, a) -> Prop (a, a) Source #

transitive_step :: Universe a => Prop (a, a) -> Prop (a, a) Source #

transitive_closure :: Universe a => Prop (a, a) -> Prop (a, a) Source #

equivalence_generated_by :: (Eq a, Universe a) => Prop (a, a) -> Prop (a, a) Source #

opposite :: Prop (a, b) -> Prop (b, a) Source #

leftAdjunct_prop :: (a -> Prop b) -> b -> Prop a Source #

Adjunction \[P^{op} \dashv P\] between functors \[P\] and \[P^{op}\], where \[P : C^{op} \Rightarrow C\] and \[P^{op} : C \Rightarrow C^{op}\]. This is based on symmetry of product in relations.

unit_prop :: b -> Prop (Prop b) Source #

rel_prop :: (a -> Bool) -> Prop a Source #

rightAdjunct of that adjunction is difficult, because it would be in C^{op}, and we don't have that category here. So how could we implement that? We'd need opposite arrow, but then the implementation would be exactly same as leftAdjunct_prop and unit_prop, but lifted to opposite category. I'm not implementing that now.

binary_rel_prop :: (a -> a -> Bool) -> Prop (a, a) Source #

binary_rel :: (a -> a -> Bool) -> a -> Prop a Source #

http://nlab.mathforge.org/nlab/show/well-founded+relation

equal_functions :: (Universe a, Eq b) => Prop (a -> b, a -> b) Source #

test_equality_at :: a -> Prop (Prop a, Prop a) Source #

equalizer_prop :: Prop a -> Prop a -> Prop a Source #

pullback_prop :: Prop a -> Prop b -> Prop (a, b) Source #

sum :: Prop a -> Prop b -> Prop (Either a b) Source #

prop_and :: Prop (Either a b) -> Prop (a, b) Source #

prop_or :: Prop (Either a b) -> Prop (a, b) Source #

prop_if :: Prop a -> Prop (Either a a) -> Prop a Source #

prop_if_general :: Prop a -> Prop (Either b c) -> Prop (a, b, c) Source #

equal :: Eq a => Prop (a, a) Source #

not_equal :: Eq a => Prop (a, a) Source #

lessthan :: Ord a => Prop (a, a) Source #

lesseq :: Ord a => Prop (a, a) Source #

or_list_prop :: Prop a -> Prop [a] Source #

and_list_prop :: Prop a -> Prop [a] Source #

enumerate :: Universe a => Prop a -> [a] Source #

existential_map :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source #

universal_map :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source #

\[universal\_map( f, p ) = \{ b | p <= f^{-1}(\{b\}) \}\]

prop_existential :: Universe b => Prop (a, b) -> Prop a Source #

prop_existential is basically the same as 'existential_map fst', except for performance. 'existential_map fst' will need to iterate over all pairs \[<a,b>\], whereas prop_existential will only iterate through all elements of b only. Similarly for prop_universal.

prop_universal :: Universe b => Prop (a, b) -> Prop a Source #

image :: Universe a => Prop (a, b) -> Prop b Source #

prop_universal_image :: (Universe a, Universe b, Eq b) => Prop (a, b) -> Prop b Source #

forevery :: Universe b => Prop b -> Prop () Source #

newtype b :\: a Source #

Constructors

PSub
Fields runpsub :: PProp a -> PProp b

data PProp a where Source #

Constructors

PProp :: Prop a -> PProp a
PNeg :: (Prop a -> Prop b) -> PProp (b :\: a)

Instances

Instances details

Contravariant PProp Source #
Instance details Defined in Math.Tools.Prop Methods contramap :: (a' -> a) -> PProp a -> PProp a' # (>$) :: b -> PProp b -> PProp a #

pneg_func :: (a -> b) -> PProp (a :\: b) Source #

module Math.Tools.Tree

module Math.Tools.Universe

module Math.Tools.Visitor