Data.Expression.Utils.Indexed.Functor

Documentation

newtype IFix f i

A fixpoint of a functor in indexed category

Constructors

IFix

Fields

• unIFix :: f (IFix f) i

Instances

IEq1 f => IEq (IFix f :: i -> Type)

Defined in Data.Expression.Utils.Indexed.Functor

Methods

ieq :: IFix f j -> IFix f j -> Bool

Heyting (ALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

neg :: ALia BooleanSort -> ALia BooleanSort

(<=>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Heyting (QFALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

neg :: QFALia BooleanSort -> QFALia BooleanSort

(<=>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Heyting (Lia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

neg :: Lia BooleanSort -> Lia BooleanSort

(<=>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Heyting (QFLia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

neg :: QFLia BooleanSort -> QFLia BooleanSort

(<=>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Heyting (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

neg :: QFLogic BooleanSort -> QFLogic BooleanSort

(<=>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Lattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

IEq1 f => Eq (IFix f i)

Defined in Data.Expression.Utils.Indexed.Functor

Methods

(==) :: IFix f i -> IFix f i -> Bool

(/=) :: IFix f i -> IFix f i -> Bool

(IFunctor f, IShow f) => Show (IFix f i)

Defined in Data.Expression.Utils.Indexed.Functor

Methods

showsPrec :: Int -> IFix f i -> ShowS

show :: IFix f i -> String

showList :: [IFix f i] -> ShowS

class IFunctor (f :: (i -> *) -> i -> *) where

A functor in indexed category

Methods

imap :: (forall i'. a i' -> b i') -> forall i'. f a i' -> f b i'

index :: forall a i'. f a i' -> Sing i'

Instances

IFunctor IfThenElseF

Defined in Data.Expression.IfThenElse

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). IfThenElseF a i' -> IfThenElseF b i'

index :: IfThenElseF a i' -> Sing i'

IFunctor ArrayF

Defined in Data.Expression.Array

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArrayF a i' -> ArrayF b i'

index :: ArrayF a i' -> Sing i'

IFunctor ArithmeticF

Defined in Data.Expression.Arithmetic

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ArithmeticF a i' -> ArithmeticF b i'

index :: ArithmeticF a i' -> Sing i'

IFunctor NegationF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). NegationF a i' -> NegationF b i'

index :: NegationF a i' -> Sing i'

IFunctor DisjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). DisjunctionF a i' -> DisjunctionF b i'

index :: DisjunctionF a i' -> Sing i'

IFunctor ConjunctionF

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ConjunctionF a i' -> ConjunctionF b i'

index :: ConjunctionF a i' -> Sing i'

IFunctor (EqualityF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression.Equality

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). EqualityF a i' -> EqualityF b i'

index :: EqualityF a i' -> Sing i'

IFunctor (ExistentialF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). ExistentialF v a i' -> ExistentialF v b i'

index :: ExistentialF v a i' -> Sing i'

IFunctor (UniversalF v :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). UniversalF v a i' -> UniversalF v b i'

index :: UniversalF v a i' -> Sing i'

IFunctor (VarF :: (Sort -> Type) -> Sort -> Type)

Defined in Data.Expression

Methods

imap :: (forall (i' :: i). a i' -> b i') -> forall (i' :: i). VarF a i' -> VarF b i'

index :: VarF a i' -> Sing i'

(IFunctor f, IFunctor g) => IFunctor (f :+: g :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

imap :: (forall (i' :: i0). a i' -> b i') -> forall (i' :: i0). (f :+: g) a i' -> (f :+: g) b i'

index :: (f :+: g) a i' -> Sing i'

icata :: IFunctor f => (forall i. f a i -> a i) -> forall i. IFix f i -> a i

Indexed catamorphism