Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Haskell.FreeTheorems.Theorems

Description

Data structures to describe theorems generated from types.

Synopsis

type Theorem = Formula
data Formula
- = ForallRelations RelationVariable (TypeExpression, TypeExpression) [Restriction] Formula
- | ForallFunctions (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Formula
- | ForallPairs (TermVariable, TermVariable) Relation Formula
- | ForallVariables TermVariable TypeExpression Formula
- | Equivalence Formula Formula
- | Implication Formula Formula
- | Conjunction Formula Formula
- | Predicate Predicate
data Restriction
- = Strict
- | Continuous
- | Total
- | BottomReflecting
- | LeftClosed
- | RespectsClasses [TypeClass]
data Predicate
- = IsMember Term Term Relation
- | IsEqual Term Term
- | IsLessEq Term Term
- | IsNotBot Term
- | IsTrue
data Term
- = TermVar TermVariable
- | TermIns Term TypeExpression
- | TermApp Term Term
- | TermComp [Term]
newtype TermVariable = TVar String
data Relation
- = RelVar RelationInfo RelationVariable
- | FunVar RelationInfo (Either Term Term)
- | RelBasic RelationInfo
- | RelLift RelationInfo TypeConstructor [Relation]
- | RelFun RelationInfo Relation Relation
- | RelFunLab RelationInfo Relation Relation
- | RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression) [Restriction] Relation
- | FunAbs RelationInfo (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Relation
relationInfo :: Relation -> RelationInfo
data RelationInfo = RelationInfo {
}
newtype RelationVariable = RVar String
data UnfoldedLift = UnfoldedLift Relation [UnfoldedDataCon]
data UnfoldedDataCon
- = BotPair
- | ConPair DataConstructor
- | ConMore DataConstructor [TermVariable] [TermVariable] Formula
data DataConstructor
- = DConEmptyList
- | DConConsList
- | DConTuple Int
- | DCon String
data UnfoldedClass = UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable) [Formula]

Documentation

type Theorem = Formula Source #

A theorem which is generated from a type signature.

data Formula Source #

Logical formula constituting automatically generated theorems.

Constructors

ForallRelations RelationVariable (TypeExpression, TypeExpression) [Restriction] Formula	Quantifies a relation variable and two type expressions.
ForallFunctions (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Formula	Quantifies a function variable and two type expressions.
ForallPairs (TermVariable, TermVariable) Relation Formula	Quantifies two term variables taken from a relation.
ForallVariables TermVariable TypeExpression Formula	Quantifies a term variable of a certain type.
Equivalence Formula Formula	Two formulas are equivalent.
Implication Formula Formula	The first formula implies the second formula.
Conjunction Formula Formula	The first formula and the second formula.
Predicate Predicate	A basic formula.

Instances

Instances details

Data Formula Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula -> c Formula #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula #

toConstr :: Formula -> Constr #

dataTypeOf :: Formula -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Formula) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula) #

gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r #

gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

data Restriction Source #

Restrictions on functions and relations.

Constructors

Strict
Continuous
Total
BottomReflecting
LeftClosed
RespectsClasses [TypeClass]

Instances

Instances details

Data Restriction Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Restriction -> c Restriction # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Restriction # toConstr :: Restriction -> Constr # dataTypeOf :: Restriction -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Restriction) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Restriction) # gmapT :: (forall b. Data b => b -> b) -> Restriction -> Restriction # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Restriction -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Restriction -> r # gmapQ :: (forall d. Data d => d -> u) -> Restriction -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Restriction -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Restriction -> m Restriction # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Restriction -> m Restriction # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Restriction -> m Restriction #
Eq Restriction Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: Restriction -> Restriction -> Bool # (/=) :: Restriction -> Restriction -> Bool #

data Predicate Source #

Predicates occurring in formulas.

Constructors

IsMember Term Term Relation	The pair of two terms is contained in a relation.
IsEqual Term Term	Two terms are equal.
IsLessEq Term Term	The first term is less defined than the second one, based on the semantical approximation order.
IsNotBot Term	The term is not equal to `_\|_`.
IsTrue	Constant True Predicate

Instances

Instances details

Data Predicate Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Predicate -> c Predicate #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Predicate #

toConstr :: Predicate -> Constr #

dataTypeOf :: Predicate -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Predicate) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Predicate) #

gmapT :: (forall b. Data b => b -> b) -> Predicate -> Predicate #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Predicate -> r #

gmapQ :: (forall d. Data d => d -> u) -> Predicate -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Predicate -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Predicate -> m Predicate #

data Term Source #

Terms consisting of variables, applications and instantiations.

Constructors

TermVar TermVariable	A term variable.
TermIns Term TypeExpression	Instantiation of a term.
TermApp Term Term	Application of a term to a term.
TermComp [Term]	Composition of function terms

Instances

Instances details

Data Term Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term # toConstr :: Term -> Constr # dataTypeOf :: Term -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) # gmapT :: (forall b. Data b => b -> b) -> Term -> Term # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r # gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term #
Eq Term Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #

newtype TermVariable Source #

Variables occurring in terms.

Constructors

TVar String

Instances

Instances details

Data TermVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermVariable -> c TermVariable # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermVariable # toConstr :: TermVariable -> Constr # dataTypeOf :: TermVariable -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermVariable) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermVariable) # gmapT :: (forall b. Data b => b -> b) -> TermVariable -> TermVariable # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermVariable -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermVariable -> r # gmapQ :: (forall d. Data d => d -> u) -> TermVariable -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TermVariable -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermVariable -> m TermVariable # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermVariable -> m TermVariable # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermVariable -> m TermVariable #
Eq TermVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: TermVariable -> TermVariable -> Bool # (/=) :: TermVariable -> TermVariable -> Bool #

data Relation Source #

Relations are the foundations of free theorems.

Constructors

RelVar RelationInfo RelationVariable	A relation variable.
FunVar RelationInfo (Either Term Term)	A function variable. It might be either a function to be applied on the left side (in equational and inequational cases) or on the right side (in inequational cases only). In inequational cases, the term is additionally composed with the semantic approximation partial order.
RelBasic RelationInfo	A basic relation corresponding to a nullary type constructor. Depending on the theorem type, this can be either an equivalence relation or the semantic approximation partial order.
RelLift RelationInfo TypeConstructor [Relation]	A lifted relation for any nonnullary type constructor. The semantics of lifted relations is differs with the language subset: In inequational subsets lifted relations explicitly require left-closedness by composition with the semantic approximation partial order. In equational subsets with fix or seq, this relation requires strictness explicitly by relating the undefined value with itself.
RelFun RelationInfo Relation Relation	A relation corresponding to a function type constructor. The semantics of this relation differs with the language subset: In the equational subset with seq, this relation is explicitly requiring bottom-reflectiveness of its members. In the inequational subset with seq, this relation is explicitly requiring totality of its members.
RelFunLab RelationInfo Relation Relation	A relation corresponding to a function type constructor. The semantics of this relation differs with the language subset: Apart from the equational subset with seq, it is equal to RelFun. In the equational subset with Seq, this relation is _not_ explicitly requiring bottom-reflectiveness of its members.
RelAbs RelationInfo RelationVariable (TypeExpression, TypeExpression) [Restriction] Relation	A relation corresponding to a type abstraction.
FunAbs RelationInfo (Either TermVariable TermVariable) (TypeExpression, TypeExpression) [Restriction] Relation	A quantified function.

Instances

Instances details

Data Relation Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Relation -> c Relation # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relation # toConstr :: Relation -> Constr # dataTypeOf :: Relation -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relation) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relation) # gmapT :: (forall b. Data b => b -> b) -> Relation -> Relation # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relation -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relation -> r # gmapQ :: (forall d. Data d => d -> u) -> Relation -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Relation -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relation -> m Relation # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relation -> m Relation # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relation -> m Relation #
Eq Relation Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: Relation -> Relation -> Bool # (/=) :: Relation -> Relation -> Bool #

relationInfo :: Relation -> RelationInfo Source #

Extracts the relation information from a relation.

data RelationInfo Source #

The relation information stored with every relation.

Constructors

RelationInfo
Fields relationLanguageSubset :: LanguageSubset The language subset in which a relation was generated. relationLeftType :: TypeExpression The type of the first components of pairs contained in a relation. relationRightType :: TypeExpression The type of the second components of pairs contained in a relation.

Instances

Instances details

Data RelationInfo Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelationInfo -> c RelationInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RelationInfo # toConstr :: RelationInfo -> Constr # dataTypeOf :: RelationInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RelationInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelationInfo) # gmapT :: (forall b. Data b => b -> b) -> RelationInfo -> RelationInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelationInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelationInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> RelationInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RelationInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationInfo -> m RelationInfo #
Eq RelationInfo Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: RelationInfo -> RelationInfo -> Bool # (/=) :: RelationInfo -> RelationInfo -> Bool #

newtype RelationVariable Source #

A relation variable.

Constructors

RVar String

Instances

Instances details

Data RelationVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelationVariable -> c RelationVariable # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RelationVariable # toConstr :: RelationVariable -> Constr # dataTypeOf :: RelationVariable -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RelationVariable) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelationVariable) # gmapT :: (forall b. Data b => b -> b) -> RelationVariable -> RelationVariable # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelationVariable -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelationVariable -> r # gmapQ :: (forall d. Data d => d -> u) -> RelationVariable -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RelationVariable -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelationVariable -> m RelationVariable # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationVariable -> m RelationVariable # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationVariable -> m RelationVariable #
Eq RelationVariable Source #
Instance details Defined in Language.Haskell.FreeTheorems.Theorems Methods (==) :: RelationVariable -> RelationVariable -> Bool # (/=) :: RelationVariable -> RelationVariable -> Bool #

data UnfoldedLift Source #

Describes unfolded lift relations.

Constructors

UnfoldedLift Relation [UnfoldedDataCon]

Instances

Instances details

Data UnfoldedLift Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnfoldedLift -> c UnfoldedLift #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnfoldedLift #

toConstr :: UnfoldedLift -> Constr #

dataTypeOf :: UnfoldedLift -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnfoldedLift) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnfoldedLift) #

gmapT :: (forall b. Data b => b -> b) -> UnfoldedLift -> UnfoldedLift #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedLift -> r #

gmapQ :: (forall d. Data d => d -> u) -> UnfoldedLift -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnfoldedLift -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedLift -> m UnfoldedLift #

data UnfoldedDataCon Source #

A relational descriptions of a data constructor.

Constructors

BotPair
ConPair DataConstructor
ConMore DataConstructor [TermVariable] [TermVariable] Formula

Instances

Instances details

Data UnfoldedDataCon Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnfoldedDataCon -> c UnfoldedDataCon #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnfoldedDataCon #

toConstr :: UnfoldedDataCon -> Constr #

dataTypeOf :: UnfoldedDataCon -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnfoldedDataCon) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnfoldedDataCon) #

gmapT :: (forall b. Data b => b -> b) -> UnfoldedDataCon -> UnfoldedDataCon #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedDataCon -> r #

gmapQ :: (forall d. Data d => d -> u) -> UnfoldedDataCon -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnfoldedDataCon -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnfoldedDataCon -> m UnfoldedDataCon #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedDataCon -> m UnfoldedDataCon #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedDataCon -> m UnfoldedDataCon #

data DataConstructor Source #

Data constructors.

Constructors

DConEmptyList	The nullary data constructor `[]`.
DConConsList	The binary data constructor `:`.
DConTuple Int	The n-ary tuple data constructor.
DCon String	Any other data constructor.

Instances

Instances details

Data DataConstructor Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataConstructor -> c DataConstructor #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataConstructor #

toConstr :: DataConstructor -> Constr #

dataTypeOf :: DataConstructor -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataConstructor) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataConstructor) #

gmapT :: (forall b. Data b => b -> b) -> DataConstructor -> DataConstructor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataConstructor -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataConstructor -> r #

gmapQ :: (forall d. Data d => d -> u) -> DataConstructor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataConstructor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataConstructor -> m DataConstructor #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConstructor -> m DataConstructor #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataConstructor -> m DataConstructor #

data UnfoldedClass Source #

A relational description of a class declaration.

Constructors

UnfoldedClass [TypeClass] TypeClass (Either RelationVariable TermVariable) [Formula]

Instances

Instances details

Data UnfoldedClass Source #

Instance details

Defined in Language.Haskell.FreeTheorems.Theorems

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnfoldedClass -> c UnfoldedClass #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnfoldedClass #

toConstr :: UnfoldedClass -> Constr #

dataTypeOf :: UnfoldedClass -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnfoldedClass) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnfoldedClass) #

gmapT :: (forall b. Data b => b -> b) -> UnfoldedClass -> UnfoldedClass #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnfoldedClass -> r #

gmapQ :: (forall d. Data d => d -> u) -> UnfoldedClass -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnfoldedClass -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnfoldedClass -> m UnfoldedClass #