-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Expressions and Formulae a la carte
--   
--   This package is aimed at providing means of fixing a first-order
--   language and declaring sorted expressions and formulae, the types
--   ensure the declared expressions fall within the language.
--   
--   This package pre-defines the common logical symbols for conjunction,
--   disjunction, negation, and universal and existential quantification as
--   well as some specific non-logical symbols such as equality, addition
--   of linear integer arithmetic, and other. Common languages such as Lia
--   and ALia (standard linear integer arithmetic and linear integer
--   arithmetic with arrays) come included.
--   
--   An example of a formula declaration:
--   
--   <pre>
--   -- Let's state that zero is successor to no integer (while this would be
--   -- true for non-negative integers, stated this way it is clearly false, but
--   -- it still is a well-formed first-order statement)
--   
--   forall [var "x" :: Var 'IntegralSort] (cnst 0 ./=. var "x" .+. cnst 1) :: Lia 'BooleanSort
--   </pre>
--   
--   Let's see what declarations the library rejects:
--   
--   <pre>
--   (var "x" :: Lia 'BooleanSort) .=. (var "y" :: Lia 'IntegralSort)
--   (var "x" :: Lia 'BooleanSort) .=. (var "y" :: ALia 'BooleanSort)
--   forall [var "x" :: Var 'IntegralSort] true :: QFLia 'BooleanSort
--   </pre>
@package expressions
@version 0.2


module Data.Expression.Utils.Indexed.Eq

-- | Indexed types that can be equated
class IEq (a :: i -> *)
ieq :: forall j. IEq a => a j -> a j -> Bool

-- | Type constructors (usually functors) that produce types that can be
--   equated
class IEq1 (f :: (i -> *) -> (i -> *))
ieq1 :: forall a j. (IEq1 f, IEq a) => f a j -> f a j -> Bool


module Data.Expression.Utils.Indexed.Foldable

-- | Type constructors (usually functors) that can be folded
class IFoldable (f :: (i -> *) -> (i -> *))
ifold :: (IFoldable f, Monoid m) => f (Const m) i' -> Const m i'


module Data.Expression.Utils.Indexed.Show

-- | <a>Show</a> for indexed type constructors (most importantly functors)
class IShow f
ishow :: IShow f => f (Const String) i -> Const String i


module Data.Expression.Utils.Indexed.Functor

-- | A fixpoint of a functor in indexed category
newtype IFix f i
IFix :: f (IFix f) i -> IFix f i
[unIFix] :: IFix f i -> f (IFix f) i

-- | A functor in indexed category
class IFunctor (f :: (i -> *) -> (i -> *))
imap :: IFunctor f => (forall i'. a i' -> b i') -> (forall i'. f a i' -> f b i')
index :: forall a i'. IFunctor f => f a i' -> Sing i'

-- | Indexed catamorphism
icata :: IFunctor f => (forall i. f a i -> a i) -> (forall i. IFix f i -> a i)
instance forall k (f :: (k -> *) -> k -> *) (i :: k). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Show.IShow f) => GHC.Show.Show (Data.Expression.Utils.Indexed.Functor.IFix f i)
instance forall i (f :: (i -> *) -> i -> *). Data.Expression.Utils.Indexed.Eq.IEq1 f => Data.Expression.Utils.Indexed.Eq.IEq (Data.Expression.Utils.Indexed.Functor.IFix f)
instance forall k (f :: (k -> *) -> k -> *) (i :: k). Data.Expression.Utils.Indexed.Eq.IEq1 f => GHC.Classes.Eq (Data.Expression.Utils.Indexed.Functor.IFix f i)


module Data.Expression.Sort

-- | A universe of recognized sorts
data Sort

-- | booleans (true, false)
BooleanSort :: Sort

-- | integers (..., -1, 0, 1, ...)
IntegralSort :: Sort

-- | arrays indexed by <a>index</a> sort, containing elements of
--   <a>element</a> sort
ArraySort :: Sort -> Sort -> Sort
[index] :: Sort -> Sort
[element] :: Sort -> Sort

-- | The singleton kind-indexed data family.

-- | Some sort (obtained for example during parsing)
data DynamicSort
[DynamicSort] :: forall (s :: Sort). Sing s -> DynamicSort

-- | An expression of some sort (obtained for example during parsing)
data DynamicallySorted (f :: (Sort -> *) -> (Sort -> *))
[DynamicallySorted] :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f

-- | Parser that accepts sort definitions such as <tt>bool</tt>,
--   <tt>int</tt>, <tt>array int int</tt>, <tt>array int (array ...)</tt>.
parseSort :: Parser DynamicSort

-- | Converts a statically sorted expression to a dynamically sorted one.
toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f

-- | Tries to convert some sort (<a>DynamicSort</a>) to a requested sort.
toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)

-- | Tries to convert an expression (<a>DynamicallySorted</a>) of some sort
--   to an expression of requested sort. Performs no conversions.
toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)
instance Data.Expression.Utils.Indexed.Eq.IEq1 f => GHC.Classes.Eq (Data.Expression.Sort.DynamicallySorted f)
instance (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Show.IShow f) => GHC.Show.Show (Data.Expression.Sort.DynamicallySorted f)
instance GHC.Classes.Eq Data.Expression.Sort.DynamicSort
instance Data.Singletons.Decide.SDecide Data.Expression.Sort.Sort => Data.Singletons.Decide.SDecide Data.Expression.Sort.Sort
instance GHC.Show.Show Data.Expression.Sort.Sort
instance GHC.Show.Show (Data.Expression.Sort.SSort s)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Expression.Sort.ArraySortSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Expression.Sort.ArraySortSym1
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Expression.Sort.IndexSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Data.Expression.Sort.ElementSym0
instance Data.Singletons.Internal.SingKind Data.Expression.Sort.Sort
instance Data.Singletons.Internal.SingI 'Data.Expression.Sort.BooleanSort
instance Data.Singletons.Internal.SingI 'Data.Expression.Sort.IntegralSort
instance (Data.Singletons.Internal.SingI n1, Data.Singletons.Internal.SingI n2) => Data.Singletons.Internal.SingI ('Data.Expression.Sort.ArraySort n1 n2)
instance GHC.Classes.Eq Data.Expression.Sort.Sort


module Data.Expression.Utils.Indexed.Traversable

-- | Type constructors (usually functors) that can be traversed
class ITraversable (t :: (i -> *) -> (i -> *))
itraverse :: forall (a :: i -> *) (b :: i -> *) f. (ITraversable t, Applicative f) => (forall (i' :: i). a i' -> f (b i')) -> (forall (i' :: i). t a i' -> f (t b i'))

-- | Maps a monadic action over a traversable functor.
imapM :: (ITraversable f, Monad m) => (forall (i' :: i). IFix f i' -> m (IFix f i')) -> (forall (i' :: i). IFix f i' -> m (IFix f i'))


module Data.Expression.Utils.Indexed.Sum

-- | Sum of two indexed functors
data ( f (:+:) g ) a i
InL :: (f a i) -> (:+:) f g a i
InR :: (g a i) -> (:+:) f g a i

-- | Inclusion relation for indexed sum functors
class (IFunctor f, IFunctor g) => f :<: g
inj :: (:<:) f g => f a i -> g a i
prj :: (:<:) f g => g a i -> Maybe (f a i)
class (IFunctor f, IFunctor g) => f :<<: g

-- | Inject a component into a sum.
inject :: g :<: f => forall i. g (IFix f) i -> IFix f i

-- | Try to unpack a sum into a component.
match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i)

-- | Embed a subset in a superset.
embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i

-- | Try to restrict a superset to a subset.
restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)
instance forall i (f :: (i -> *) -> i -> *). Data.Expression.Utils.Indexed.Functor.IFunctor f => f Data.Expression.Utils.Indexed.Sum.:<<: f
instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g) => f Data.Expression.Utils.Indexed.Sum.:<<: (g Data.Expression.Utils.Indexed.Sum.:+: f)
instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *) (h :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g, Data.Expression.Utils.Indexed.Functor.IFunctor h, f Data.Expression.Utils.Indexed.Sum.:<<: g) => f Data.Expression.Utils.Indexed.Sum.:<<: (h Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall i (f :: (i -> *) -> i -> *). Data.Expression.Utils.Indexed.Functor.IFunctor f => f Data.Expression.Utils.Indexed.Sum.:<: f
instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g) => f Data.Expression.Utils.Indexed.Sum.:<: (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *) (h :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g, Data.Expression.Utils.Indexed.Functor.IFunctor h, f Data.Expression.Utils.Indexed.Sum.:<: g) => f Data.Expression.Utils.Indexed.Sum.:<: (h Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall i (f :: (i -> *) -> i -> *) (g :: (i -> *) -> i -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g) => Data.Expression.Utils.Indexed.Functor.IFunctor (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall i (f :: (i -> *) -> i -> *) (g :: (i -> *) -> i -> *). (Data.Expression.Utils.Indexed.Eq.IEq1 f, Data.Expression.Utils.Indexed.Eq.IEq1 g) => Data.Expression.Utils.Indexed.Eq.IEq1 (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall i (f :: (i -> *) -> i -> *) (g :: (i -> *) -> i -> *). (Data.Expression.Utils.Indexed.Foldable.IFoldable f, Data.Expression.Utils.Indexed.Foldable.IFoldable g) => Data.Expression.Utils.Indexed.Foldable.IFoldable (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall i (f :: (i -> *) -> i -> *) (g :: (i -> *) -> i -> *). (Data.Expression.Utils.Indexed.Traversable.ITraversable f, Data.Expression.Utils.Indexed.Traversable.ITraversable g) => Data.Expression.Utils.Indexed.Traversable.ITraversable (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (g :: (k1 -> *) -> k2 -> *). (Data.Expression.Utils.Indexed.Show.IShow f, Data.Expression.Utils.Indexed.Show.IShow g) => Data.Expression.Utils.Indexed.Show.IShow (f Data.Expression.Utils.Indexed.Sum.:+: g)


module Data.Expression.Parser

-- | Parsing context assigning sorts to known variables
type Context = Map String DynamicSort

-- | Context-sensitive parser that remembers sorts of variables
type Parser = ReaderT Context (StateT Context Parser)

-- | Expressions that can be parsed
class Parseable f g
parser :: Parseable f g => Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)

-- | Tries to parse the entire input text and produce an expression in
--   desired language and with desired sort.
parse :: forall f (s :: Sort). (Parseable f f, SingI s) => Text -> Maybe (IFix f s)

-- | Like <a>parse</a> but allows adding initial assumption about sorts of
--   some variables.
parseWith :: forall f (s :: Sort). (Parseable f f, SingI s) => Context -> Text -> Maybe (IFix f s)

-- | Matches a given character.
char :: Char -> Parser Char

-- | Matches first of many choices.
choice :: [Parser a] -> Parser a

-- | Matches a given decimal number.
decimal :: Parser Int

-- | Matches a given digit.
digit :: Parser Char

-- | Matches any character.
letter :: Parser Char

-- | Matches one or more times.
many1 :: Parser a -> Parser [a]

-- | Matches one or more times, separated by specified separator.
sepBy1 :: Parser a -> Parser s -> Parser [a]

-- | Matches a signed number.
signed :: Parser Int -> Parser Int

-- | Matches space.
space :: Parser Char

-- | Matches a given string.
string :: Text -> Parser Text

-- | Matches identifier that starts with [a-zA-Z'_<tt>#] and is followed by
--   [a-zA-Z'_</tt>#0-9].
identifier :: Parser String

-- | Labels parser.
(<?>) :: Parser a -> String -> Parser a

-- | Asserts what sort is assigned to a variable in current context.
assertSort :: String -> DynamicSort -> Parser ()

-- | Variable assumes sort based on current context.
assumeSort :: String -> Parser DynamicSort
instance forall k1 k2 (f :: k1 -> k2 -> *) (h :: (Data.Expression.Sort.Sort -> *) -> Data.Expression.Sort.Sort -> *) (g :: k1 -> k2 -> *). (Data.Expression.Parser.Parseable f h, Data.Expression.Parser.Parseable g h) => Data.Expression.Parser.Parseable (f Data.Expression.Utils.Indexed.Sum.:+: g) h


module Data.Expression.IfThenElse

-- | A functor representing a conditional value (if-then-else)
data IfThenElseF a (s :: Sort)
[IfThenElse] :: Sing s -> a  'BooleanSort -> a s -> a s -> IfThenElseF a s

-- | A smart constructor for an if-then-else expression
ite :: forall f s. (IfThenElseF :<: f, SingI s) => IFix f  'BooleanSort -> IFix f s -> IFix f s -> IFix f s
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.IfThenElse.IfThenElseF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.IfThenElse.IfThenElseF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.IfThenElse.IfThenElseF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.IfThenElse.IfThenElseF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.IfThenElse.IfThenElseF
instance (Data.Expression.IfThenElse.IfThenElseF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.IfThenElse.IfThenElseF f


module Data.Expression.Equality

-- | A functor representing an equality predicate between two expressions
--   of matching sort
data EqualityF a (s :: Sort)
[Equals] :: Sing s -> a s -> a s -> EqualityF a  'BooleanSort

-- | A smart constructor for an equality predicate
(.=.) :: forall f s. (EqualityF :<: f, SingI s) => IFix f s -> IFix f s -> IFix f  'BooleanSort
infix 7 .=.
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.Equality.EqualityF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.Equality.EqualityF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.Equality.EqualityF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.Equality.EqualityF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.Equality.EqualityF
instance (Data.Expression.Equality.EqualityF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.Equality.EqualityF f


module Data.Expression.Array

-- | A functor representing array-theoretic terms (<a>select</a> and
--   <a>store</a> also known as "read" and "write")
data ArrayF a (s :: Sort)
[Select] :: Sing i -> Sing e -> a ( 'ArraySort i e) -> a i -> ArrayF a e
[Store] :: Sing i -> Sing e -> a ( 'ArraySort i e) -> a i -> a e -> ArrayF a ( 'ArraySort i e)

-- | A smart constructor for select
select :: (ArrayF :<: f, SingI i, SingI e) => IFix f ( 'ArraySort i e) -> IFix f i -> IFix f e

-- | A smart constructor for store
store :: (ArrayF :<: f, SingI i, SingI e) => IFix f ( 'ArraySort i e) -> IFix f i -> IFix f e -> IFix f ( 'ArraySort i e)
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.Array.ArrayF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.Array.ArrayF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.Array.ArrayF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.Array.ArrayF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.Array.ArrayF
instance (Data.Expression.Array.ArrayF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.Array.ArrayF f


module Data.Expression.Arithmetic

-- | A functor representing linear integer arithmetic: constants
--   (<a>cnst</a>), addition (<a>add</a> or <a>.+.</a>), multiplication
--   (<a>mul</a> or <a>.*.</a>), divisibility predicate (<a>.\.</a>) and
--   ordering (<a>.&lt;.</a>, <a>.&gt;.</a>, <a>.&lt;=.</a>,
--   <a>.&gt;=.</a>).
data ArithmeticF a (s :: Sort)
[Const] :: Int -> ArithmeticF a  'IntegralSort
[Add] :: [a  'IntegralSort] -> ArithmeticF a  'IntegralSort
[Mul] :: [a  'IntegralSort] -> ArithmeticF a  'IntegralSort
[Divides] :: Int -> a  'IntegralSort -> ArithmeticF a  'BooleanSort
[LessThan] :: a  'IntegralSort -> a  'IntegralSort -> ArithmeticF a  'BooleanSort

-- | A smart constructor for integer constants
cnst :: ArithmeticF :<: f => Int -> IFix f  'IntegralSort

-- | A smart constructor for a variadic addition
add :: ArithmeticF :<: f => [IFix f  'IntegralSort] -> IFix f  'IntegralSort

-- | A smart constructor for a variadic multiplication
mul :: ArithmeticF :<: f => [IFix f  'IntegralSort] -> IFix f  'IntegralSort

-- | A smart constructor for binary addition
(.+.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'IntegralSort
infixl 8 .+.

-- | A smart constructor for a binary multiplication
(.*.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'IntegralSort
infixl 9 .*.

-- | A smart constructor for a divisibility predicate
(.\.) :: ArithmeticF :<: f => Int -> IFix f  'IntegralSort -> IFix f  'BooleanSort
infix 7 .\.

-- | A smart constructor for <tt>&lt;</tt>
(.<.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'BooleanSort
infix 7 .<.

-- | A smart constructor for <tt>&gt;</tt>
(.>.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'BooleanSort
infix 7 .>.

-- | A smart constructor for <tt>&lt;=</tt>
(.<=.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'BooleanSort
infix 7 .<=.

-- | A smart constructor for <tt>&gt;=</tt>
(.>=.) :: forall f. ArithmeticF :<: f => IFix f  'IntegralSort -> IFix f  'IntegralSort -> IFix f  'BooleanSort
infix 7 .>=.
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.Arithmetic.ArithmeticF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.Arithmetic.ArithmeticF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.Arithmetic.ArithmeticF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.Arithmetic.ArithmeticF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.Arithmetic.ArithmeticF
instance (Data.Expression.Arithmetic.ArithmeticF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.Arithmetic.ArithmeticF f


-- | Usage:
--   
--   You can build expressions in predefined languages (<a>QFLogic</a>,
--   <a>QFLia</a>, <a>QFALia</a>, <a>Lia</a>, <a>ALia</a>) using the smart
--   constructors such as <a>var</a>, <a>and</a>, <a>or</a>, <a>not</a>,
--   <a>forall</a>, <a>exists</a> (or operators <a>.&amp;.</a>, <a>.|.</a>,
--   <a>.-&gt;.</a>, <a>.&lt;-.</a>, <a>.&lt;-&gt;.</a>) or you can define
--   your own sorted language as a fixpoint (<a>IFix</a>) of a sum
--   (<a>:+:</a>) of indexed functors (<a>IFunctor</a>).
module Data.Expression

-- | The singleton kind-indexed data family.

-- | A universe of recognized sorts
data Sort

-- | booleans (true, false)
BooleanSort :: Sort

-- | integers (..., -1, 0, 1, ...)
IntegralSort :: Sort

-- | arrays indexed by <a>index</a> sort, containing elements of
--   <a>element</a> sort
ArraySort :: Sort -> Sort -> Sort

-- | An expression of some sort (obtained for example during parsing)
data DynamicallySorted (f :: (Sort -> *) -> (Sort -> *))
[DynamicallySorted] :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f

-- | Some sort (obtained for example during parsing)
data DynamicSort
[DynamicSort] :: forall (s :: Sort). Sing s -> DynamicSort

-- | Tries to convert some sort (<a>DynamicSort</a>) to a requested sort.
toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)

-- | Converts a statically sorted expression to a dynamically sorted one.
toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f

-- | Tries to convert an expression (<a>DynamicallySorted</a>) of some sort
--   to an expression of requested sort. Performs no conversions.
toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)

-- | Parser that accepts sort definitions such as <tt>bool</tt>,
--   <tt>int</tt>, <tt>array int int</tt>, <tt>array int (array ...)</tt>.
parseSort :: Parser DynamicSort

-- | A functor representing propositional logic embedded in first order
--   logic (quantifier-free, boolean variables aka propositions, logical
--   connectives <a>and</a>, <a>or</a>, <a>not</a>, equality of
--   propositions)
type QFLogicF = EqualityF :+: ConjunctionF :+: DisjunctionF :+: NegationF :+: VarF

-- | A functor representing the language of quantifier-free linear integer
--   arithmetic theory in first order logic (integer constants, integer
--   variables, addition, multiplication, divisibility, ordering)
type QFLiaF = ArithmeticF :+: IfThenElseF :+: QFLogicF

-- | A functor much like <a>QFLiaF</a> with quantifiers over booleans and
--   integers
type LiaF = ExistentialF  'BooleanSort :+: ExistentialF  'IntegralSort :+: UniversalF  'BooleanSort :+: UniversalF  'IntegralSort :+: QFLiaF

-- | A functor representing the language of quantifier-free linear integer
--   arithmetic and array theories in first order logic (much like
--   <a>QFLiaF</a> with additional array variables, <a>select</a>, and
--   <a>store</a>)
type QFALiaF = ArrayF :+: QFLiaF

-- | A functor much like <a>QFALiaF</a> with quantifiers over booleans and
--   integers
type ALiaF = ExistentialF  'BooleanSort :+: ExistentialF  'IntegralSort :+: UniversalF  'BooleanSort :+: UniversalF  'IntegralSort :+: QFALiaF

-- | A language consisting solely of variables (useful for listing
--   variables outside of any particular context, such as bound variables
--   of quantified formula)
type Var = IFix VarF

-- | A language obtained as fixpoint of <a>QFLogicF</a>
type QFLogic = IFix QFLogicF

-- | A language obtained as fixpoint of <a>QFLiaF</a>
type QFLia = IFix QFLiaF

-- | A language obtained as fixpoint of <a>LiaF</a>
type Lia = IFix LiaF

-- | A language obtained as fixpoint of <a>QFALiaF</a>
type QFALia = IFix QFALiaF

-- | A language obtained as fixpoint of <a>ALiaF</a>
type ALia = IFix ALiaF

-- | Bounded lattices that support complementing elements
--   
--   <pre>
--   complement . complement = id
--   </pre>
class BoundedLattice a => ComplementedLattice a
complement :: ComplementedLattice a => a -> a

-- | Type of names assigned to variables
type VariableName = String

-- | A functor representing a sorted variable, each variable is identified
--   by its name and sort
data VarF a (s :: Sort)
[Var] :: VariableName -> Sing s -> VarF a s

-- | A functor representing a logical connective for conjunction
data ConjunctionF a (s :: Sort)
[And] :: [a  'BooleanSort] -> ConjunctionF a  'BooleanSort

-- | A functor representing a logical connective for disjunction
data DisjunctionF a (s :: Sort)
[Or] :: [a  'BooleanSort] -> DisjunctionF a  'BooleanSort

-- | A functor representing a logical connective for negation
data NegationF a (s :: Sort)
[Not] :: a  'BooleanSort -> NegationF a  'BooleanSort

-- | A functor representing a mono-sorted universal quantifier binding a
--   number of variables within a formula
data UniversalF (v :: Sort) a (s :: Sort)
[Forall] :: [Var v] -> a  'BooleanSort -> UniversalF v a  'BooleanSort

-- | A functor representing a mono-sorted existential quantifier binding a
--   number of variables within a formula
data ExistentialF (v :: Sort) a (s :: Sort)
[Exists] :: [Var v] -> a  'BooleanSort -> ExistentialF v a  'BooleanSort

-- | Substitution that given an expression produces replacement if the
--   expression is to be replaced or nothing otherwise.
newtype Substitution f
Substitution :: forall (s :: Sort). IFix f s -> Maybe (IFix f s) -> Substitution f
[runSubstitution] :: Substitution f -> forall (s :: Sort). IFix f s -> Maybe (IFix f s)

-- | Executes a substitution.
substitute :: (IFunctor f, IEq1 f) => IFix f s -> Substitution f -> IFix f s

-- | A simple constructor of substitutions that replaces the latter
--   expression with the former.
for :: forall f (s :: Sort). (IFunctor f, IEq1 f) => IFix f s -> IFix f s -> Substitution f

-- | A smart constructor for variables of any sort in any language Takes
--   the variable name and infers the target language and sort from
--   context.
--   
--   <pre>
--   var "a" :: Lia 'IntegralSort
--   </pre>
var :: forall f s. (VarF :<: f, SingI s) => VariableName -> IFix f s

-- | Logical tautology
true :: ConjunctionF :<: f => IFix f  'BooleanSort

-- | Logical contradiction
false :: DisjunctionF :<: f => IFix f  'BooleanSort

-- | A smart constructor for variadic conjunction
and :: ConjunctionF :<: f => [IFix f  'BooleanSort] -> IFix f  'BooleanSort

-- | A smart constructor for variadic disjunction
or :: DisjunctionF :<: f => [IFix f  'BooleanSort] -> IFix f  'BooleanSort

-- | A smart constructor for negation
not :: NegationF :<: f => IFix f  'BooleanSort -> IFix f  'BooleanSort

-- | A smart constructor for universally quantified formulae
forall :: UniversalF v :<: f => [Var v] -> IFix f  'BooleanSort -> IFix f  'BooleanSort

-- | A smart constructor for existentially quantified formulae
exists :: ExistentialF v :<: f => [Var v] -> IFix f  'BooleanSort -> IFix f  'BooleanSort

-- | A smart constructor for binary conjunction
(.&.) :: ConjunctionF :<: f => IFix f  'BooleanSort -> IFix f  'BooleanSort -> IFix f  'BooleanSort
infixr 6 .&.

-- | A smart constructor for binary disjunction
(.|.) :: DisjunctionF :<: f => IFix f  'BooleanSort -> IFix f  'BooleanSort -> IFix f  'BooleanSort
infixr 5 .|.

-- | A smart constructor for implication (an abbreviation for <tt>not a .|.
--   b</tt>)
(.->.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f  'BooleanSort -> IFix f  'BooleanSort -> IFix f  'BooleanSort
infixr 4 .->.

-- | A smart constructor for reversed implication (an abbreviation for
--   <tt>a .|. not b</tt>)
(.<-.) :: (DisjunctionF :<: f, NegationF :<: f) => IFix f  'BooleanSort -> IFix f  'BooleanSort -> IFix f  'BooleanSort
infixl 4 .<-.

-- | A smart constructor for if-and-only-if connective
(.<->.) :: (ConjunctionF :<: f, DisjunctionF :<: f, NegationF :<: f) => IFix f  'BooleanSort -> IFix f  'BooleanSort -> IFix f  'BooleanSort
infix 3 .<->.

-- | A smart constructor for disequality
(./=.) :: forall f s. (NegationF :<: f, EqualityF :<: f, SingI s) => IFix f s -> IFix f s -> IFix f  'BooleanSort
infix 7 ./=.

-- | <a>literals</a> decomposes a boolean combination (formed with
--   conjunctions and disjunctions, preferably in negation normal form)
--   into its constituents.
literals :: (ConjunctionF :<: f, DisjunctionF :<: f) => IFix f  'BooleanSort -> [IFix f  'BooleanSort]

-- | <a>conjuncts</a> decomposes a conjunction into conjuncts.
conjuncts :: ConjunctionF :<: f => IFix f  'BooleanSort -> [IFix f  'BooleanSort]

-- | <a>disjuncts</a> decomposes a disjunction into disjuncts.
disjuncts :: DisjunctionF :<: f => IFix f  'BooleanSort -> [IFix f  'BooleanSort]

-- | Collects a list of all variables occurring in an expression (bound or
--   free).
vars :: (VarF :<: f, IFoldable f, IFunctor f) => IFix f s -> [DynamicallySorted VarF]

-- | Collects a list of all free variables occurring in an expression.
freevars :: (IFunctor f, MaybeQuantified f) => IFix f s -> [DynamicallySorted VarF]
class MaybeQuantified f

-- | Test whether an expression contains a quantifier.
isQuantified :: MaybeQuantified f => IFix f s -> Bool

-- | Tests whether an expression is free of any quantifier.
isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool
class (NegationF :<: f, HasDual f f) => NNF f

-- | Propagates negation toward boolean atoms (across conjunction,
--   disjunction, quantifiers).
nnf :: forall f. NNF f => IFix f  'BooleanSort -> IFix f  'BooleanSort
class (VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f) => Prenex f

-- | Puts an expression into prenex form (quantifier prefix and a
--   quantifier-free formula).
prenex :: forall f. Prenex f => IFix f  'BooleanSort -> IFix f  'BooleanSort
class (VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f) => Flatten f

-- | Replaces non-variable and non-constant arguments to uninterpreted
--   functions (such as <a>select</a> and <a>store</a>) with a fresh bound
--   (universally or existentially) variable that is bound to the original
--   term.
flatten :: forall f. Flatten f => IFix f  'BooleanSort -> IFix f  'BooleanSort
class (VarF :<: f, EqualityF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f) => Unstore f

-- | Replaces <a>store</a> with an instance of its axiomatization.
unstore :: forall f. Unstore f => IFix f  'BooleanSort -> IFix f  'BooleanSort
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.Equality.EqualityF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.Bind f f, Data.Expression.Bind' f f, Data.Expression.MaybeQuantified'' f f, Data.Expression.Forall f f, Data.Expression.Axiomatized f f, Data.Expression.Utils.Indexed.Foldable.IFoldable f, Data.Expression.Utils.Indexed.Traversable.ITraversable f) => Data.Expression.Unstore f
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.ConjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.DisjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Equality.EqualityF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Array.ArrayF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Axiomatized Data.Expression.Array.ArrayF g
instance (Data.Expression.Axiomatized f h, Data.Expression.Axiomatized g h) => Data.Expression.Axiomatized (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance Data.Expression.Axiomatized f g
instance (Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Singletons.Internal.SingI v) => Data.Expression.Forall (Data.Expression.UniversalF v) g
instance forall k1 k2 (f :: k1 -> k2 -> *) (h :: (Data.Expression.Sort.Sort -> *) -> Data.Expression.Sort.Sort -> *) (g :: k1 -> k2 -> *). (Data.Expression.Forall f h, Data.Expression.Forall g h) => Data.Expression.Forall (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance forall k (f :: k) (g :: (Data.Expression.Sort.Sort -> *) -> Data.Expression.Sort.Sort -> *). Data.Expression.Forall f g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.Bind f f, Data.Expression.Bind' f f, Data.Expression.MaybeQuantified'' f f, Data.Expression.Utils.Indexed.Foldable.IFoldable f, Data.Expression.Utils.Indexed.Traversable.ITraversable f) => Data.Expression.Flatten f
instance (Data.Expression.Array.ArrayF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.MaybeQuantified'' Data.Expression.Array.ArrayF g
instance (Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Singletons.Internal.SingI v) => Data.Expression.MaybeQuantified'' (Data.Expression.UniversalF v) g
instance (Data.Expression.ExistentialF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Singletons.Internal.SingI v) => Data.Expression.MaybeQuantified'' (Data.Expression.ExistentialF v) g
instance (Data.Expression.MaybeQuantified'' f h, Data.Expression.MaybeQuantified'' g h) => Data.Expression.MaybeQuantified'' (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance (f Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.MaybeQuantified'' f g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Bind' Data.Expression.VarF g
instance (Data.Expression.Arithmetic.ArithmeticF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Bind' Data.Expression.Arithmetic.ArithmeticF g
instance (Data.Expression.ConjunctionF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Bind' Data.Expression.ConjunctionF g
instance (Data.Expression.DisjunctionF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Bind' Data.Expression.DisjunctionF g
instance (Data.Expression.Bind' f h, Data.Expression.Bind' g h) => Data.Expression.Bind' (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance (f Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.Bind' f g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Equality.EqualityF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.DisjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.MaybeQuantified g, Data.Singletons.Internal.SingI v) => Data.Expression.Bind (Data.Expression.UniversalF v) g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Equality.EqualityF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.ConjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.ExistentialF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.MaybeQuantified g, Data.Singletons.Internal.SingI v) => Data.Expression.Bind (Data.Expression.ExistentialF v) g
instance forall k1 k2 (f :: k1 -> k2 -> *) (h :: (Data.Expression.Sort.Sort -> *) -> Data.Expression.Sort.Sort -> *) (g :: k1 -> k2 -> *). (Data.Expression.Bind f h, Data.Expression.Bind g h) => Data.Expression.Bind (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance forall k (f :: k) (g :: (Data.Expression.Sort.Sort -> *) -> Data.Expression.Sort.Sort -> *). Data.Expression.Bind f g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Foldable.IFoldable f, Data.Expression.Utils.Indexed.Traversable.ITraversable f, Data.Expression.HasDual f f, Data.Expression.MaybeQuantified' f f) => Data.Expression.Prenex f
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Utils.Indexed.Eq.IEq1 g) => Data.Expression.MaybeQuantified' (Data.Expression.UniversalF v) g
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.ExistentialF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Utils.Indexed.Eq.IEq1 g) => Data.Expression.MaybeQuantified' (Data.Expression.ExistentialF v) g
instance (Data.Expression.MaybeQuantified' f h, Data.Expression.MaybeQuantified' g h) => Data.Expression.MaybeQuantified' (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance (f Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.Utils.Indexed.Foldable.IFoldable f) => Data.Expression.MaybeQuantified' f g
instance (Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: f, Data.Expression.HasDual f f) => Data.Expression.NNF f
instance Data.Expression.HasDual Data.Expression.NegationF g
instance (Data.Expression.DisjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.HasDual g g) => Data.Expression.HasDual Data.Expression.ConjunctionF g
instance (Data.Expression.ConjunctionF Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.HasDual g g) => Data.Expression.HasDual Data.Expression.DisjunctionF g
instance (Data.Expression.ExistentialF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.HasDual g g) => Data.Expression.HasDual (Data.Expression.UniversalF v) g
instance (Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.HasDual g g) => Data.Expression.HasDual (Data.Expression.ExistentialF v) g
instance (Data.Expression.HasDual f h, Data.Expression.HasDual g h) => Data.Expression.HasDual (f Data.Expression.Utils.Indexed.Sum.:+: g) h
instance (f Data.Expression.Utils.Indexed.Sum.:<: g, Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: g) => Data.Expression.HasDual f g
instance Data.Expression.MaybeQuantified Data.Expression.VarF
instance Data.Expression.MaybeQuantified (Data.Expression.UniversalF v)
instance Data.Expression.MaybeQuantified (Data.Expression.ExistentialF v)
instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *). (Data.Expression.MaybeQuantified f, Data.Expression.MaybeQuantified g) => Data.Expression.MaybeQuantified (f Data.Expression.Utils.Indexed.Sum.:+: g)
instance forall k (f :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Foldable.IFoldable f) => Data.Expression.MaybeQuantified f
instance Algebra.Lattice.JoinSemiLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.MeetSemiLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.Lattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedJoinSemiLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedMeetSemiLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.ComplementedLattice (Data.Expression.Lia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.JoinSemiLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.MeetSemiLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.Lattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedJoinSemiLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedMeetSemiLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.ComplementedLattice (Data.Expression.ALia 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.Utils.Indexed.Eq.IEq1 (Data.Expression.ExistentialF v)
instance Data.Expression.Utils.Indexed.Functor.IFunctor (Data.Expression.ExistentialF v)
instance Data.Expression.Utils.Indexed.Foldable.IFoldable (Data.Expression.ExistentialF v)
instance Data.Expression.Utils.Indexed.Traversable.ITraversable (Data.Expression.ExistentialF v)
instance Data.Expression.Utils.Indexed.Show.IShow (Data.Expression.ExistentialF v)
instance (Data.Expression.ExistentialF v Data.Expression.Utils.Indexed.Sum.:<: f, Data.Singletons.Internal.SingI v) => Data.Expression.Parser.Parseable (Data.Expression.ExistentialF v) f
instance Data.Expression.Utils.Indexed.Eq.IEq1 (Data.Expression.UniversalF v)
instance Data.Expression.Utils.Indexed.Functor.IFunctor (Data.Expression.UniversalF v)
instance Data.Expression.Utils.Indexed.Foldable.IFoldable (Data.Expression.UniversalF v)
instance Data.Expression.Utils.Indexed.Traversable.ITraversable (Data.Expression.UniversalF v)
instance Data.Expression.Utils.Indexed.Show.IShow (Data.Expression.UniversalF v)
instance (Data.Expression.UniversalF v Data.Expression.Utils.Indexed.Sum.:<: f, Data.Singletons.Internal.SingI v) => Data.Expression.Parser.Parseable (Data.Expression.UniversalF v) f
instance Algebra.Lattice.JoinSemiLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.MeetSemiLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.Lattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedJoinSemiLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedMeetSemiLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.ComplementedLattice (Data.Expression.QFALia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.JoinSemiLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.MeetSemiLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.Lattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedJoinSemiLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedMeetSemiLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.ComplementedLattice (Data.Expression.QFLia 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.JoinSemiLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.MeetSemiLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.Lattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedJoinSemiLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedMeetSemiLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Algebra.Lattice.BoundedLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.ComplementedLattice (Data.Expression.QFLogic 'Data.Expression.Sort.BooleanSort)
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.NegationF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.NegationF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.NegationF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.NegationF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.NegationF
instance (Data.Expression.NegationF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.NegationF f
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.DisjunctionF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.DisjunctionF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.DisjunctionF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.DisjunctionF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.DisjunctionF
instance (Data.Expression.DisjunctionF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.DisjunctionF f
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.ConjunctionF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.ConjunctionF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.ConjunctionF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.ConjunctionF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.ConjunctionF
instance (Data.Expression.ConjunctionF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.ConjunctionF f
instance GHC.Base.Semigroup (Data.Expression.Substitution f)
instance GHC.Base.Monoid (Data.Expression.Substitution f)
instance Data.Expression.Utils.Indexed.Eq.IEq1 Data.Expression.VarF
instance Data.Expression.Utils.Indexed.Functor.IFunctor Data.Expression.VarF
instance Data.Expression.Utils.Indexed.Foldable.IFoldable Data.Expression.VarF
instance Data.Expression.Utils.Indexed.Traversable.ITraversable Data.Expression.VarF
instance Data.Expression.Utils.Indexed.Show.IShow Data.Expression.VarF
instance (Data.Expression.VarF Data.Expression.Utils.Indexed.Sum.:<: f) => Data.Expression.Parser.Parseable Data.Expression.VarF f