Copyright	(c) Eugen Kuksa University of Magdeburg 2017
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability	provisional
Portability	portable
Safe Haskell	None

TPTP.AS

Description

Definition of abstract syntax for TPTP taken from [1]

References

1

G. Sutcliffe et al.: The TPTP language grammar in BNF. http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html

Note: The implemented version is saved at TPTPDocumentsSyntaxBNF.html

Note: The names of the data types are aligned with the names of the grammar rules at this reference page (modulo case).

2

C. Kaliszyk, G. Sutcliffe and F. Rabe: TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism https://kwarc.info/people/frabe/Research/KRS_thf1_16.pdf Note: for further information on TF0, TF1, TH0 and TH1

Documentation

newtype BASIC_SPEC Source #

Constructors

Basic_spec [Annoted TPTP]

Instances

Eq BASIC_SPEC Source #
Methods (==) :: BASIC_SPEC -> BASIC_SPEC -> Bool (/=) :: BASIC_SPEC -> BASIC_SPEC -> Bool
Data BASIC_SPEC Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_SPEC -> c BASIC_SPEC gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_SPEC toConstr :: BASIC_SPEC -> Constr dataTypeOf :: BASIC_SPEC -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_SPEC) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_SPEC) gmapT :: (forall b. Data b => b -> b) -> BASIC_SPEC -> BASIC_SPEC gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC
Ord BASIC_SPEC Source #
Methods compare :: BASIC_SPEC -> BASIC_SPEC -> Ordering (<) :: BASIC_SPEC -> BASIC_SPEC -> Bool (<=) :: BASIC_SPEC -> BASIC_SPEC -> Bool (>) :: BASIC_SPEC -> BASIC_SPEC -> Bool (>=) :: BASIC_SPEC -> BASIC_SPEC -> Bool max :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC min :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
Show BASIC_SPEC Source #
Methods showsPrec :: Int -> BASIC_SPEC -> ShowS show :: BASIC_SPEC -> String showList :: [BASIC_SPEC] -> ShowS
GetRange BASIC_SPEC Source #
Methods getRange :: BASIC_SPEC -> Range Source # rangeSpan :: BASIC_SPEC -> [Pos] Source #
Syntax TPTP BASIC_SPEC Symbol () () Source #
Methods parsersAndPrinters :: TPTP -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: TPTP -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: TPTP -> Maybe (AParser st ()) Source # parse_symb_items :: TPTP -> Maybe (AParser st ()) Source # parse_symb_map_items :: TPTP -> Maybe (AParser st ()) Source # toItem :: TPTP -> BASIC_SPEC -> Item Source # symb_items_name :: TPTP -> () -> [String] Source #
StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source #
Methods basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source # sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source # stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source # convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source # ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: TPTP -> Symbol -> () Source # id_to_raw :: TPTP -> Id -> () Source # matches :: TPTP -> Symbol -> () -> Bool Source # empty_signature :: TPTP -> Sign Source # add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source # signature_union :: TPTP -> Sign -> Sign -> Result Sign Source # signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source # intersection :: TPTP -> Sign -> Sign -> Result Sign Source # final_union :: TPTP -> Sign -> Sign -> Result Sign Source # morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: TPTP -> Sign -> Sign -> Bool Source # subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source # generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: TPTP -> Morphism -> Bool Source # is_injective :: TPTP -> Morphism -> Bool Source # theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source #
Methods parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source # stability :: TPTP -> Stability Source # data_logic :: TPTP -> Maybe AnyLogic Source # top_sublogic :: TPTP -> Sublogic Source # all_sublogics :: TPTP -> [Sublogic] Source # bottomSublogic :: TPTP -> Maybe Sublogic Source # sublogicDimensions :: TPTP -> [[Sublogic]] Source # parseSublogic :: TPTP -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source # provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source # default_prover :: TPTP -> String Source # cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source # conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source # empty_proof_tree :: TPTP -> ProofTree Source # syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: TPTP -> Maybe OMCD Source # export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #

newtype TPTP Source #

Constructors

TPTP [TPTP_input]

Instances

Eq TPTP Source #
Methods (==) :: TPTP -> TPTP -> Bool (/=) :: TPTP -> TPTP -> Bool
Data TPTP Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP -> c TPTP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPTP toConstr :: TPTP -> Constr dataTypeOf :: TPTP -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TPTP) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPTP) gmapT :: (forall b. Data b => b -> b) -> TPTP -> TPTP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP -> r gmapQ :: (forall d. Data d => d -> u) -> TPTP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP
Ord TPTP Source #
Methods compare :: TPTP -> TPTP -> Ordering (<) :: TPTP -> TPTP -> Bool (<=) :: TPTP -> TPTP -> Bool (>) :: TPTP -> TPTP -> Bool (>=) :: TPTP -> TPTP -> Bool max :: TPTP -> TPTP -> TPTP min :: TPTP -> TPTP -> TPTP
Show TPTP Source #
Methods showsPrec :: Int -> TPTP -> ShowS show :: TPTP -> String showList :: [TPTP] -> ShowS
GetRange TPTP Source #
Methods getRange :: TPTP -> Range Source # rangeSpan :: TPTP -> [Pos] Source #

data TPTP_input Source #

Constructors

Annotated_formula Annotated_formula
TPTP_include Include
TPTP_comment Comment
TPTP_defined_comment DefinedComment
TPTP_system_comment SystemComment

Instances

Eq TPTP_input Source #
Methods (==) :: TPTP_input -> TPTP_input -> Bool (/=) :: TPTP_input -> TPTP_input -> Bool
Data TPTP_input Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP_input -> c TPTP_input gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPTP_input toConstr :: TPTP_input -> Constr dataTypeOf :: TPTP_input -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TPTP_input) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPTP_input) gmapT :: (forall b. Data b => b -> b) -> TPTP_input -> TPTP_input gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_input -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_input -> r gmapQ :: (forall d. Data d => d -> u) -> TPTP_input -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP_input -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP_input -> m TPTP_input gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_input -> m TPTP_input gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_input -> m TPTP_input
Ord TPTP_input Source #
Methods compare :: TPTP_input -> TPTP_input -> Ordering (<) :: TPTP_input -> TPTP_input -> Bool (<=) :: TPTP_input -> TPTP_input -> Bool (>) :: TPTP_input -> TPTP_input -> Bool (>=) :: TPTP_input -> TPTP_input -> Bool max :: TPTP_input -> TPTP_input -> TPTP_input min :: TPTP_input -> TPTP_input -> TPTP_input
Show TPTP_input Source #
Methods showsPrec :: Int -> TPTP_input -> ShowS show :: TPTP_input -> String showList :: [TPTP_input] -> ShowS
GetRange TPTP_input Source #
Methods getRange :: TPTP_input -> Range Source # rangeSpan :: TPTP_input -> [Pos] Source #

data Comment Source #

Constructors

Comment_line Token
Comment_block Token

Instances

Eq Comment Source #
Methods (==) :: Comment -> Comment -> Bool (/=) :: Comment -> Comment -> Bool
Data Comment Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comment -> c Comment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comment toConstr :: Comment -> Constr dataTypeOf :: Comment -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Comment) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comment) gmapT :: (forall b. Data b => b -> b) -> Comment -> Comment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comment -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comment -> r gmapQ :: (forall d. Data d => d -> u) -> Comment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Comment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comment -> m Comment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comment -> m Comment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comment -> m Comment
Ord Comment Source #
Methods compare :: Comment -> Comment -> Ordering (<) :: Comment -> Comment -> Bool (<=) :: Comment -> Comment -> Bool (>) :: Comment -> Comment -> Bool (>=) :: Comment -> Comment -> Bool max :: Comment -> Comment -> Comment min :: Comment -> Comment -> Comment
Show Comment Source #
Methods showsPrec :: Int -> Comment -> ShowS show :: Comment -> String showList :: [Comment] -> ShowS
GetRange Comment Source #
Methods getRange :: Comment -> Range Source # rangeSpan :: Comment -> [Pos] Source #

data DefinedComment Source #

Constructors

Defined_comment_line Token
Defined_comment_block Token

Instances

Eq DefinedComment Source #
Methods (==) :: DefinedComment -> DefinedComment -> Bool (/=) :: DefinedComment -> DefinedComment -> Bool
Data DefinedComment Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedComment -> c DefinedComment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedComment toConstr :: DefinedComment -> Constr dataTypeOf :: DefinedComment -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c DefinedComment) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedComment) gmapT :: (forall b. Data b => b -> b) -> DefinedComment -> DefinedComment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedComment -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedComment -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedComment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedComment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment
Ord DefinedComment Source #
Methods compare :: DefinedComment -> DefinedComment -> Ordering (<) :: DefinedComment -> DefinedComment -> Bool (<=) :: DefinedComment -> DefinedComment -> Bool (>) :: DefinedComment -> DefinedComment -> Bool (>=) :: DefinedComment -> DefinedComment -> Bool max :: DefinedComment -> DefinedComment -> DefinedComment min :: DefinedComment -> DefinedComment -> DefinedComment
Show DefinedComment Source #
Methods showsPrec :: Int -> DefinedComment -> ShowS show :: DefinedComment -> String showList :: [DefinedComment] -> ShowS
GetRange DefinedComment Source #
Methods getRange :: DefinedComment -> Range Source # rangeSpan :: DefinedComment -> [Pos] Source #

data SystemComment Source #

Constructors

System_comment_line Token
System_comment_block Token

Instances

Eq SystemComment Source #
Methods (==) :: SystemComment -> SystemComment -> Bool (/=) :: SystemComment -> SystemComment -> Bool
Data SystemComment Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SystemComment -> c SystemComment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SystemComment toConstr :: SystemComment -> Constr dataTypeOf :: SystemComment -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SystemComment) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SystemComment) gmapT :: (forall b. Data b => b -> b) -> SystemComment -> SystemComment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SystemComment -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SystemComment -> r gmapQ :: (forall d. Data d => d -> u) -> SystemComment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SystemComment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment
Ord SystemComment Source #
Methods compare :: SystemComment -> SystemComment -> Ordering (<) :: SystemComment -> SystemComment -> Bool (<=) :: SystemComment -> SystemComment -> Bool (>) :: SystemComment -> SystemComment -> Bool (>=) :: SystemComment -> SystemComment -> Bool max :: SystemComment -> SystemComment -> SystemComment min :: SystemComment -> SystemComment -> SystemComment
Show SystemComment Source #
Methods showsPrec :: Int -> SystemComment -> ShowS show :: SystemComment -> String showList :: [SystemComment] -> ShowS
GetRange SystemComment Source #
Methods getRange :: SystemComment -> Range Source # rangeSpan :: SystemComment -> [Pos] Source #

data Annotated_formula Source #

Constructors

AF_THF_Annotated THF_annotated
AF_TFX_Annotated TFX_annotated
AF_TFF_Annotated TFF_annotated
AF_TCF_Annotated TCF_annotated
AF_FOF_Annotated FOF_annotated
AF_CNF_Annotated CNF_annotated
AF_TPI_Annotated TPI_annotated

Instances

Eq Annotated_formula Source #
Methods (==) :: Annotated_formula -> Annotated_formula -> Bool (/=) :: Annotated_formula -> Annotated_formula -> Bool
Data Annotated_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotated_formula -> c Annotated_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotated_formula toConstr :: Annotated_formula -> Constr dataTypeOf :: Annotated_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Annotated_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotated_formula) gmapT :: (forall b. Data b => b -> b) -> Annotated_formula -> Annotated_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotated_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotated_formula -> r gmapQ :: (forall d. Data d => d -> u) -> Annotated_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotated_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotated_formula -> m Annotated_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotated_formula -> m Annotated_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotated_formula -> m Annotated_formula
Ord Annotated_formula Source #
Methods compare :: Annotated_formula -> Annotated_formula -> Ordering (<) :: Annotated_formula -> Annotated_formula -> Bool (<=) :: Annotated_formula -> Annotated_formula -> Bool (>) :: Annotated_formula -> Annotated_formula -> Bool (>=) :: Annotated_formula -> Annotated_formula -> Bool max :: Annotated_formula -> Annotated_formula -> Annotated_formula min :: Annotated_formula -> Annotated_formula -> Annotated_formula
Show Annotated_formula Source #
Methods showsPrec :: Int -> Annotated_formula -> ShowS show :: Annotated_formula -> String showList :: [Annotated_formula] -> ShowS
GetRange Annotated_formula Source #
Methods getRange :: Annotated_formula -> Range Source # rangeSpan :: Annotated_formula -> [Pos] Source #
Sentences TPTP Sentence Sign Morphism Symbol Source #
Methods map_sen :: TPTP -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: TPTP -> Sign -> Sentence -> Sentence Source # negation :: TPTP -> Sentence -> Maybe Sentence Source # print_sign :: TPTP -> Sign -> Doc Source # print_named :: TPTP -> Named Sentence -> Doc Source # sym_of :: TPTP -> Sign -> [Set Symbol] Source # mostSymsOf :: TPTP -> Sign -> [Symbol] Source # symmap_of :: TPTP -> Morphism -> EndoMap Symbol Source # sym_name :: TPTP -> Symbol -> Id Source # sym_label :: TPTP -> Symbol -> Maybe String Source # fullSymName :: TPTP -> Symbol -> String Source # symKind :: TPTP -> Symbol -> String Source # symsOfSen :: TPTP -> Sign -> Sentence -> [Symbol] Source # pair_symbols :: TPTP -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source #
Methods basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source # sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source # stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source # convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source # ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: TPTP -> Symbol -> () Source # id_to_raw :: TPTP -> Id -> () Source # matches :: TPTP -> Symbol -> () -> Bool Source # empty_signature :: TPTP -> Sign Source # add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source # signature_union :: TPTP -> Sign -> Sign -> Result Sign Source # signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source # intersection :: TPTP -> Sign -> Sign -> Result Sign Source # final_union :: TPTP -> Sign -> Sign -> Result Sign Source # morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: TPTP -> Sign -> Sign -> Bool Source # subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source # generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: TPTP -> Morphism -> Bool Source # is_injective :: TPTP -> Morphism -> Bool Source # theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source #
Methods parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source # stability :: TPTP -> Stability Source # data_logic :: TPTP -> Maybe AnyLogic Source # top_sublogic :: TPTP -> Sublogic Source # all_sublogics :: TPTP -> [Sublogic] Source # bottomSublogic :: TPTP -> Maybe Sublogic Source # sublogicDimensions :: TPTP -> [[Sublogic]] Source # parseSublogic :: TPTP -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source # provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source # default_prover :: TPTP -> String Source # cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source # conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source # empty_proof_tree :: TPTP -> ProofTree Source # syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: TPTP -> Maybe OMCD Source # export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #

data TPI_annotated Source #

Constructors

TPI_annotated Name Formula_role TPI_formula Annotations

Instances

Eq TPI_annotated Source #
Methods (==) :: TPI_annotated -> TPI_annotated -> Bool (/=) :: TPI_annotated -> TPI_annotated -> Bool
Data TPI_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPI_annotated -> c TPI_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPI_annotated toConstr :: TPI_annotated -> Constr dataTypeOf :: TPI_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TPI_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPI_annotated) gmapT :: (forall b. Data b => b -> b) -> TPI_annotated -> TPI_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPI_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPI_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> TPI_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TPI_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPI_annotated -> m TPI_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPI_annotated -> m TPI_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPI_annotated -> m TPI_annotated
Ord TPI_annotated Source #
Methods compare :: TPI_annotated -> TPI_annotated -> Ordering (<) :: TPI_annotated -> TPI_annotated -> Bool (<=) :: TPI_annotated -> TPI_annotated -> Bool (>) :: TPI_annotated -> TPI_annotated -> Bool (>=) :: TPI_annotated -> TPI_annotated -> Bool max :: TPI_annotated -> TPI_annotated -> TPI_annotated min :: TPI_annotated -> TPI_annotated -> TPI_annotated
Show TPI_annotated Source #
Methods showsPrec :: Int -> TPI_annotated -> ShowS show :: TPI_annotated -> String showList :: [TPI_annotated] -> ShowS
GetRange TPI_annotated Source #
Methods getRange :: TPI_annotated -> Range Source # rangeSpan :: TPI_annotated -> [Pos] Source #

type TPI_formula = FOF_formula Source #

data THF_annotated Source #

Constructors

THF_annotated Name Formula_role THF_formula Annotations

Instances

Eq THF_annotated Source #
Methods (==) :: THF_annotated -> THF_annotated -> Bool (/=) :: THF_annotated -> THF_annotated -> Bool
Data THF_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_annotated -> c THF_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_annotated toConstr :: THF_annotated -> Constr dataTypeOf :: THF_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_annotated) gmapT :: (forall b. Data b => b -> b) -> THF_annotated -> THF_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> THF_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_annotated -> m THF_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_annotated -> m THF_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_annotated -> m THF_annotated
Ord THF_annotated Source #
Methods compare :: THF_annotated -> THF_annotated -> Ordering (<) :: THF_annotated -> THF_annotated -> Bool (<=) :: THF_annotated -> THF_annotated -> Bool (>) :: THF_annotated -> THF_annotated -> Bool (>=) :: THF_annotated -> THF_annotated -> Bool max :: THF_annotated -> THF_annotated -> THF_annotated min :: THF_annotated -> THF_annotated -> THF_annotated
Show THF_annotated Source #
Methods showsPrec :: Int -> THF_annotated -> ShowS show :: THF_annotated -> String showList :: [THF_annotated] -> ShowS
GetRange THF_annotated Source #
Methods getRange :: THF_annotated -> Range Source # rangeSpan :: THF_annotated -> [Pos] Source #

data TFX_annotated Source #

Constructors

TFX_annotated Name Formula_role TFX_formula Annotations

Instances

Eq TFX_annotated Source #
Methods (==) :: TFX_annotated -> TFX_annotated -> Bool (/=) :: TFX_annotated -> TFX_annotated -> Bool
Data TFX_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFX_annotated -> c TFX_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFX_annotated toConstr :: TFX_annotated -> Constr dataTypeOf :: TFX_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFX_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFX_annotated) gmapT :: (forall b. Data b => b -> b) -> TFX_annotated -> TFX_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFX_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFX_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> TFX_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFX_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFX_annotated -> m TFX_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_annotated -> m TFX_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_annotated -> m TFX_annotated
Ord TFX_annotated Source #
Methods compare :: TFX_annotated -> TFX_annotated -> Ordering (<) :: TFX_annotated -> TFX_annotated -> Bool (<=) :: TFX_annotated -> TFX_annotated -> Bool (>) :: TFX_annotated -> TFX_annotated -> Bool (>=) :: TFX_annotated -> TFX_annotated -> Bool max :: TFX_annotated -> TFX_annotated -> TFX_annotated min :: TFX_annotated -> TFX_annotated -> TFX_annotated
Show TFX_annotated Source #
Methods showsPrec :: Int -> TFX_annotated -> ShowS show :: TFX_annotated -> String showList :: [TFX_annotated] -> ShowS
GetRange TFX_annotated Source #
Methods getRange :: TFX_annotated -> Range Source # rangeSpan :: TFX_annotated -> [Pos] Source #

data TFF_annotated Source #

Constructors

TFF_annotated Name Formula_role TFF_formula Annotations

Instances

Eq TFF_annotated Source #
Methods (==) :: TFF_annotated -> TFF_annotated -> Bool (/=) :: TFF_annotated -> TFF_annotated -> Bool
Data TFF_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_annotated -> c TFF_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_annotated toConstr :: TFF_annotated -> Constr dataTypeOf :: TFF_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_annotated) gmapT :: (forall b. Data b => b -> b) -> TFF_annotated -> TFF_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_annotated -> m TFF_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_annotated -> m TFF_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_annotated -> m TFF_annotated
Ord TFF_annotated Source #
Methods compare :: TFF_annotated -> TFF_annotated -> Ordering (<) :: TFF_annotated -> TFF_annotated -> Bool (<=) :: TFF_annotated -> TFF_annotated -> Bool (>) :: TFF_annotated -> TFF_annotated -> Bool (>=) :: TFF_annotated -> TFF_annotated -> Bool max :: TFF_annotated -> TFF_annotated -> TFF_annotated min :: TFF_annotated -> TFF_annotated -> TFF_annotated
Show TFF_annotated Source #
Methods showsPrec :: Int -> TFF_annotated -> ShowS show :: TFF_annotated -> String showList :: [TFF_annotated] -> ShowS
GetRange TFF_annotated Source #
Methods getRange :: TFF_annotated -> Range Source # rangeSpan :: TFF_annotated -> [Pos] Source #

data TCF_annotated Source #

Constructors

TCF_annotated Name Formula_role TCF_formula Annotations

Instances

Eq TCF_annotated Source #
Methods (==) :: TCF_annotated -> TCF_annotated -> Bool (/=) :: TCF_annotated -> TCF_annotated -> Bool
Data TCF_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCF_annotated -> c TCF_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCF_annotated toConstr :: TCF_annotated -> Constr dataTypeOf :: TCF_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TCF_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCF_annotated) gmapT :: (forall b. Data b => b -> b) -> TCF_annotated -> TCF_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCF_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCF_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> TCF_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TCF_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCF_annotated -> m TCF_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_annotated -> m TCF_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_annotated -> m TCF_annotated
Ord TCF_annotated Source #
Methods compare :: TCF_annotated -> TCF_annotated -> Ordering (<) :: TCF_annotated -> TCF_annotated -> Bool (<=) :: TCF_annotated -> TCF_annotated -> Bool (>) :: TCF_annotated -> TCF_annotated -> Bool (>=) :: TCF_annotated -> TCF_annotated -> Bool max :: TCF_annotated -> TCF_annotated -> TCF_annotated min :: TCF_annotated -> TCF_annotated -> TCF_annotated
Show TCF_annotated Source #
Methods showsPrec :: Int -> TCF_annotated -> ShowS show :: TCF_annotated -> String showList :: [TCF_annotated] -> ShowS
GetRange TCF_annotated Source #
Methods getRange :: TCF_annotated -> Range Source # rangeSpan :: TCF_annotated -> [Pos] Source #

data FOF_annotated Source #

Constructors

FOF_annotated Name Formula_role FOF_formula Annotations

Instances

Eq FOF_annotated Source #
Methods (==) :: FOF_annotated -> FOF_annotated -> Bool (/=) :: FOF_annotated -> FOF_annotated -> Bool
Data FOF_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_annotated -> c FOF_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_annotated toConstr :: FOF_annotated -> Constr dataTypeOf :: FOF_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_annotated) gmapT :: (forall b. Data b => b -> b) -> FOF_annotated -> FOF_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_annotated -> m FOF_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_annotated -> m FOF_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_annotated -> m FOF_annotated
Ord FOF_annotated Source #
Methods compare :: FOF_annotated -> FOF_annotated -> Ordering (<) :: FOF_annotated -> FOF_annotated -> Bool (<=) :: FOF_annotated -> FOF_annotated -> Bool (>) :: FOF_annotated -> FOF_annotated -> Bool (>=) :: FOF_annotated -> FOF_annotated -> Bool max :: FOF_annotated -> FOF_annotated -> FOF_annotated min :: FOF_annotated -> FOF_annotated -> FOF_annotated
Show FOF_annotated Source #
Methods showsPrec :: Int -> FOF_annotated -> ShowS show :: FOF_annotated -> String showList :: [FOF_annotated] -> ShowS
GetRange FOF_annotated Source #
Methods getRange :: FOF_annotated -> Range Source # rangeSpan :: FOF_annotated -> [Pos] Source #

data CNF_annotated Source #

Constructors

CNF_annotated Name Formula_role CNF_formula Annotations

Instances

Eq CNF_annotated Source #
Methods (==) :: CNF_annotated -> CNF_annotated -> Bool (/=) :: CNF_annotated -> CNF_annotated -> Bool
Data CNF_annotated Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CNF_annotated -> c CNF_annotated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CNF_annotated toConstr :: CNF_annotated -> Constr dataTypeOf :: CNF_annotated -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c CNF_annotated) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CNF_annotated) gmapT :: (forall b. Data b => b -> b) -> CNF_annotated -> CNF_annotated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CNF_annotated -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CNF_annotated -> r gmapQ :: (forall d. Data d => d -> u) -> CNF_annotated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CNF_annotated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CNF_annotated -> m CNF_annotated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CNF_annotated -> m CNF_annotated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CNF_annotated -> m CNF_annotated
Ord CNF_annotated Source #
Methods compare :: CNF_annotated -> CNF_annotated -> Ordering (<) :: CNF_annotated -> CNF_annotated -> Bool (<=) :: CNF_annotated -> CNF_annotated -> Bool (>) :: CNF_annotated -> CNF_annotated -> Bool (>=) :: CNF_annotated -> CNF_annotated -> Bool max :: CNF_annotated -> CNF_annotated -> CNF_annotated min :: CNF_annotated -> CNF_annotated -> CNF_annotated
Show CNF_annotated Source #
Methods showsPrec :: Int -> CNF_annotated -> ShowS show :: CNF_annotated -> String showList :: [CNF_annotated] -> ShowS
GetRange CNF_annotated Source #
Methods getRange :: CNF_annotated -> Range Source # rangeSpan :: CNF_annotated -> [Pos] Source #

name :: Annotated_formula -> Name Source #

formulaRole :: Annotated_formula -> Formula_role Source #

annotations :: Annotated_formula -> Annotations Source #

newtype Annotations Source #

Constructors

Annotations (Maybe (Source, Optional_info))

Instances

Eq Annotations Source #
Methods (==) :: Annotations -> Annotations -> Bool (/=) :: Annotations -> Annotations -> Bool
Data Annotations Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotations -> c Annotations gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotations toConstr :: Annotations -> Constr dataTypeOf :: Annotations -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Annotations) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotations) gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations
Ord Annotations Source #
Methods compare :: Annotations -> Annotations -> Ordering (<) :: Annotations -> Annotations -> Bool (<=) :: Annotations -> Annotations -> Bool (>) :: Annotations -> Annotations -> Bool (>=) :: Annotations -> Annotations -> Bool max :: Annotations -> Annotations -> Annotations min :: Annotations -> Annotations -> Annotations
Show Annotations Source #
Methods showsPrec :: Int -> Annotations -> ShowS show :: Annotations -> String showList :: [Annotations] -> ShowS
GetRange Annotations Source #
Methods getRange :: Annotations -> Range Source # rangeSpan :: Annotations -> [Pos] Source #

data Formula_role Source #

Constructors

Axiom
Hypothesis
Definition
Assumption
Lemma
Theorem
Corollary
Conjecture
Negated_conjecture
Plain
Type
Fi_domain
Fi_functors
Fi_predicates
Unknown
Other_formula_role Token	For future updates. Should not be used.

Instances

Eq Formula_role Source #
Methods (==) :: Formula_role -> Formula_role -> Bool (/=) :: Formula_role -> Formula_role -> Bool
Data Formula_role Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula_role -> c Formula_role gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula_role toConstr :: Formula_role -> Constr dataTypeOf :: Formula_role -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Formula_role) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula_role) gmapT :: (forall b. Data b => b -> b) -> Formula_role -> Formula_role gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula_role -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula_role -> r gmapQ :: (forall d. Data d => d -> u) -> Formula_role -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula_role -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula_role -> m Formula_role gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula_role -> m Formula_role gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula_role -> m Formula_role
Ord Formula_role Source #
Methods compare :: Formula_role -> Formula_role -> Ordering (<) :: Formula_role -> Formula_role -> Bool (<=) :: Formula_role -> Formula_role -> Bool (>) :: Formula_role -> Formula_role -> Bool (>=) :: Formula_role -> Formula_role -> Bool max :: Formula_role -> Formula_role -> Formula_role min :: Formula_role -> Formula_role -> Formula_role
Show Formula_role Source #
Methods showsPrec :: Int -> Formula_role -> ShowS show :: Formula_role -> String showList :: [Formula_role] -> ShowS
GetRange Formula_role Source #
Methods getRange :: Formula_role -> Range Source # rangeSpan :: Formula_role -> [Pos] Source #

data THF_formula Source #

Constructors

THFF_logic THF_logic_formula
THFF_sequent THF_sequent

Instances

Eq THF_formula Source #
Methods (==) :: THF_formula -> THF_formula -> Bool (/=) :: THF_formula -> THF_formula -> Bool
Data THF_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_formula -> c THF_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_formula toConstr :: THF_formula -> Constr dataTypeOf :: THF_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_formula) gmapT :: (forall b. Data b => b -> b) -> THF_formula -> THF_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_formula -> m THF_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_formula -> m THF_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_formula -> m THF_formula
Ord THF_formula Source #
Methods compare :: THF_formula -> THF_formula -> Ordering (<) :: THF_formula -> THF_formula -> Bool (<=) :: THF_formula -> THF_formula -> Bool (>) :: THF_formula -> THF_formula -> Bool (>=) :: THF_formula -> THF_formula -> Bool max :: THF_formula -> THF_formula -> THF_formula min :: THF_formula -> THF_formula -> THF_formula
Show THF_formula Source #
Methods showsPrec :: Int -> THF_formula -> ShowS show :: THF_formula -> String showList :: [THF_formula] -> ShowS
GetRange THF_formula Source #
Methods getRange :: THF_formula -> Range Source # rangeSpan :: THF_formula -> [Pos] Source #

data THF_logic_formula Source #

Constructors

THFLF_binary THF_binary_formula
THFLF_unitary THF_unitary_formula
THFLF_type THF_type_formula
THFLF_subtype THF_subtype

Instances

Eq THF_logic_formula Source #
Methods (==) :: THF_logic_formula -> THF_logic_formula -> Bool (/=) :: THF_logic_formula -> THF_logic_formula -> Bool
Data THF_logic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_logic_formula -> c THF_logic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_logic_formula toConstr :: THF_logic_formula -> Constr dataTypeOf :: THF_logic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_logic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_logic_formula) gmapT :: (forall b. Data b => b -> b) -> THF_logic_formula -> THF_logic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_logic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_logic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_logic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_logic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_logic_formula -> m THF_logic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_logic_formula -> m THF_logic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_logic_formula -> m THF_logic_formula
Ord THF_logic_formula Source #
Methods compare :: THF_logic_formula -> THF_logic_formula -> Ordering (<) :: THF_logic_formula -> THF_logic_formula -> Bool (<=) :: THF_logic_formula -> THF_logic_formula -> Bool (>) :: THF_logic_formula -> THF_logic_formula -> Bool (>=) :: THF_logic_formula -> THF_logic_formula -> Bool max :: THF_logic_formula -> THF_logic_formula -> THF_logic_formula min :: THF_logic_formula -> THF_logic_formula -> THF_logic_formula
Show THF_logic_formula Source #
Methods showsPrec :: Int -> THF_logic_formula -> ShowS show :: THF_logic_formula -> String showList :: [THF_logic_formula] -> ShowS
GetRange THF_logic_formula Source #
Methods getRange :: THF_logic_formula -> Range Source # rangeSpan :: THF_logic_formula -> [Pos] Source #

data THF_binary_formula Source #

Constructors

THFBF_pair THF_binary_pair
THFBF_tuple THF_binary_tuple

Instances

Eq THF_binary_formula Source #
Methods (==) :: THF_binary_formula -> THF_binary_formula -> Bool (/=) :: THF_binary_formula -> THF_binary_formula -> Bool
Data THF_binary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_binary_formula -> c THF_binary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_binary_formula toConstr :: THF_binary_formula -> Constr dataTypeOf :: THF_binary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_binary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_binary_formula) gmapT :: (forall b. Data b => b -> b) -> THF_binary_formula -> THF_binary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_binary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_binary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_binary_formula -> m THF_binary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_formula -> m THF_binary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_formula -> m THF_binary_formula
Ord THF_binary_formula Source #
Methods compare :: THF_binary_formula -> THF_binary_formula -> Ordering (<) :: THF_binary_formula -> THF_binary_formula -> Bool (<=) :: THF_binary_formula -> THF_binary_formula -> Bool (>) :: THF_binary_formula -> THF_binary_formula -> Bool (>=) :: THF_binary_formula -> THF_binary_formula -> Bool max :: THF_binary_formula -> THF_binary_formula -> THF_binary_formula min :: THF_binary_formula -> THF_binary_formula -> THF_binary_formula
Show THF_binary_formula Source #
Methods showsPrec :: Int -> THF_binary_formula -> ShowS show :: THF_binary_formula -> String showList :: [THF_binary_formula] -> ShowS
GetRange THF_binary_formula Source #
Methods getRange :: THF_binary_formula -> Range Source # rangeSpan :: THF_binary_formula -> [Pos] Source #

data THF_binary_pair Source #

Constructors

THF_binary_pair THF_pair_connective THF_unitary_formula THF_unitary_formula

Instances

Eq THF_binary_pair Source #
Methods (==) :: THF_binary_pair -> THF_binary_pair -> Bool (/=) :: THF_binary_pair -> THF_binary_pair -> Bool
Data THF_binary_pair Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_binary_pair -> c THF_binary_pair gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_binary_pair toConstr :: THF_binary_pair -> Constr dataTypeOf :: THF_binary_pair -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_binary_pair) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_binary_pair) gmapT :: (forall b. Data b => b -> b) -> THF_binary_pair -> THF_binary_pair gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_pair -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_pair -> r gmapQ :: (forall d. Data d => d -> u) -> THF_binary_pair -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_binary_pair -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_binary_pair -> m THF_binary_pair gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_pair -> m THF_binary_pair gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_pair -> m THF_binary_pair
Ord THF_binary_pair Source #
Methods compare :: THF_binary_pair -> THF_binary_pair -> Ordering (<) :: THF_binary_pair -> THF_binary_pair -> Bool (<=) :: THF_binary_pair -> THF_binary_pair -> Bool (>) :: THF_binary_pair -> THF_binary_pair -> Bool (>=) :: THF_binary_pair -> THF_binary_pair -> Bool max :: THF_binary_pair -> THF_binary_pair -> THF_binary_pair min :: THF_binary_pair -> THF_binary_pair -> THF_binary_pair
Show THF_binary_pair Source #
Methods showsPrec :: Int -> THF_binary_pair -> ShowS show :: THF_binary_pair -> String showList :: [THF_binary_pair] -> ShowS
GetRange THF_binary_pair Source #
Methods getRange :: THF_binary_pair -> Range Source # rangeSpan :: THF_binary_pair -> [Pos] Source #

data THF_binary_tuple Source #

Constructors

THFBT_or THF_or_formula
THFBT_and THF_and_formula
THFBT_apply THF_apply_formula

Instances

Eq THF_binary_tuple Source #
Methods (==) :: THF_binary_tuple -> THF_binary_tuple -> Bool (/=) :: THF_binary_tuple -> THF_binary_tuple -> Bool
Data THF_binary_tuple Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_binary_tuple -> c THF_binary_tuple gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_binary_tuple toConstr :: THF_binary_tuple -> Constr dataTypeOf :: THF_binary_tuple -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_binary_tuple) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_binary_tuple) gmapT :: (forall b. Data b => b -> b) -> THF_binary_tuple -> THF_binary_tuple gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_tuple -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_tuple -> r gmapQ :: (forall d. Data d => d -> u) -> THF_binary_tuple -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_binary_tuple -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_binary_tuple -> m THF_binary_tuple gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_tuple -> m THF_binary_tuple gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_tuple -> m THF_binary_tuple
Ord THF_binary_tuple Source #
Methods compare :: THF_binary_tuple -> THF_binary_tuple -> Ordering (<) :: THF_binary_tuple -> THF_binary_tuple -> Bool (<=) :: THF_binary_tuple -> THF_binary_tuple -> Bool (>) :: THF_binary_tuple -> THF_binary_tuple -> Bool (>=) :: THF_binary_tuple -> THF_binary_tuple -> Bool max :: THF_binary_tuple -> THF_binary_tuple -> THF_binary_tuple min :: THF_binary_tuple -> THF_binary_tuple -> THF_binary_tuple
Show THF_binary_tuple Source #
Methods showsPrec :: Int -> THF_binary_tuple -> ShowS show :: THF_binary_tuple -> String showList :: [THF_binary_tuple] -> ShowS
GetRange THF_binary_tuple Source #
Methods getRange :: THF_binary_tuple -> Range Source # rangeSpan :: THF_binary_tuple -> [Pos] Source #

type THF_or_formula = [THF_unitary_formula] Source #

type THF_and_formula = [THF_unitary_formula] Source #

type THF_apply_formula = [THF_unitary_formula] Source #

data THF_unitary_formula Source #

Constructors

THFUF_quantified THF_quantified_formula
THFUF_unary THF_unary_formula
THFUF_atom THF_atom
THFUF_conditional THF_conditional
THFUF_let THF_let
THFUF_tuple THF_tuple
THFUF_logic THF_logic_formula

Instances

Eq THF_unitary_formula Source #
Methods (==) :: THF_unitary_formula -> THF_unitary_formula -> Bool (/=) :: THF_unitary_formula -> THF_unitary_formula -> Bool
Data THF_unitary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_unitary_formula -> c THF_unitary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_unitary_formula toConstr :: THF_unitary_formula -> Constr dataTypeOf :: THF_unitary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_unitary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_unitary_formula) gmapT :: (forall b. Data b => b -> b) -> THF_unitary_formula -> THF_unitary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_unitary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_unitary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_unitary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_unitary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_unitary_formula -> m THF_unitary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unitary_formula -> m THF_unitary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unitary_formula -> m THF_unitary_formula
Ord THF_unitary_formula Source #
Methods compare :: THF_unitary_formula -> THF_unitary_formula -> Ordering (<) :: THF_unitary_formula -> THF_unitary_formula -> Bool (<=) :: THF_unitary_formula -> THF_unitary_formula -> Bool (>) :: THF_unitary_formula -> THF_unitary_formula -> Bool (>=) :: THF_unitary_formula -> THF_unitary_formula -> Bool max :: THF_unitary_formula -> THF_unitary_formula -> THF_unitary_formula min :: THF_unitary_formula -> THF_unitary_formula -> THF_unitary_formula
Show THF_unitary_formula Source #
Methods showsPrec :: Int -> THF_unitary_formula -> ShowS show :: THF_unitary_formula -> String showList :: [THF_unitary_formula] -> ShowS
GetRange THF_unitary_formula Source #
Methods getRange :: THF_unitary_formula -> Range Source # rangeSpan :: THF_unitary_formula -> [Pos] Source #

data THF_quantified_formula Source #

Constructors

THF_quantified_formula THF_quantification THF_unitary_formula

Instances

Eq THF_quantified_formula Source #
Methods (==) :: THF_quantified_formula -> THF_quantified_formula -> Bool (/=) :: THF_quantified_formula -> THF_quantified_formula -> Bool
Data THF_quantified_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_quantified_formula -> c THF_quantified_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_quantified_formula toConstr :: THF_quantified_formula -> Constr dataTypeOf :: THF_quantified_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_quantified_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_quantified_formula) gmapT :: (forall b. Data b => b -> b) -> THF_quantified_formula -> THF_quantified_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_quantified_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_quantified_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_quantified_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_quantified_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_quantified_formula -> m THF_quantified_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_quantified_formula -> m THF_quantified_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_quantified_formula -> m THF_quantified_formula
Ord THF_quantified_formula Source #
Methods compare :: THF_quantified_formula -> THF_quantified_formula -> Ordering (<) :: THF_quantified_formula -> THF_quantified_formula -> Bool (<=) :: THF_quantified_formula -> THF_quantified_formula -> Bool (>) :: THF_quantified_formula -> THF_quantified_formula -> Bool (>=) :: THF_quantified_formula -> THF_quantified_formula -> Bool max :: THF_quantified_formula -> THF_quantified_formula -> THF_quantified_formula min :: THF_quantified_formula -> THF_quantified_formula -> THF_quantified_formula
Show THF_quantified_formula Source #
Methods showsPrec :: Int -> THF_quantified_formula -> ShowS show :: THF_quantified_formula -> String showList :: [THF_quantified_formula] -> ShowS
GetRange THF_quantified_formula Source #
Methods getRange :: THF_quantified_formula -> Range Source # rangeSpan :: THF_quantified_formula -> [Pos] Source #

data THF_quantification Source #

Constructors

THF_quantification THF_quantifier THF_variable_list

Instances

Eq THF_quantification Source #
Methods (==) :: THF_quantification -> THF_quantification -> Bool (/=) :: THF_quantification -> THF_quantification -> Bool
Data THF_quantification Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_quantification -> c THF_quantification gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_quantification toConstr :: THF_quantification -> Constr dataTypeOf :: THF_quantification -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_quantification) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_quantification) gmapT :: (forall b. Data b => b -> b) -> THF_quantification -> THF_quantification gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_quantification -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_quantification -> r gmapQ :: (forall d. Data d => d -> u) -> THF_quantification -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_quantification -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_quantification -> m THF_quantification gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_quantification -> m THF_quantification gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_quantification -> m THF_quantification
Ord THF_quantification Source #
Methods compare :: THF_quantification -> THF_quantification -> Ordering (<) :: THF_quantification -> THF_quantification -> Bool (<=) :: THF_quantification -> THF_quantification -> Bool (>) :: THF_quantification -> THF_quantification -> Bool (>=) :: THF_quantification -> THF_quantification -> Bool max :: THF_quantification -> THF_quantification -> THF_quantification min :: THF_quantification -> THF_quantification -> THF_quantification
Show THF_quantification Source #
Methods showsPrec :: Int -> THF_quantification -> ShowS show :: THF_quantification -> String showList :: [THF_quantification] -> ShowS
GetRange THF_quantification Source #
Methods getRange :: THF_quantification -> Range Source # rangeSpan :: THF_quantification -> [Pos] Source #

type THF_variable_list = [THF_variable] Source #

data THF_variable Source #

Constructors

THFV_typed THF_typed_variable
THFV_variable Variable

Instances

Eq THF_variable Source #
Methods (==) :: THF_variable -> THF_variable -> Bool (/=) :: THF_variable -> THF_variable -> Bool
Data THF_variable Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_variable -> c THF_variable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_variable toConstr :: THF_variable -> Constr dataTypeOf :: THF_variable -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_variable) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_variable) gmapT :: (forall b. Data b => b -> b) -> THF_variable -> THF_variable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_variable -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_variable -> r gmapQ :: (forall d. Data d => d -> u) -> THF_variable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_variable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_variable -> m THF_variable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_variable -> m THF_variable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_variable -> m THF_variable
Ord THF_variable Source #
Methods compare :: THF_variable -> THF_variable -> Ordering (<) :: THF_variable -> THF_variable -> Bool (<=) :: THF_variable -> THF_variable -> Bool (>) :: THF_variable -> THF_variable -> Bool (>=) :: THF_variable -> THF_variable -> Bool max :: THF_variable -> THF_variable -> THF_variable min :: THF_variable -> THF_variable -> THF_variable
Show THF_variable Source #
Methods showsPrec :: Int -> THF_variable -> ShowS show :: THF_variable -> String showList :: [THF_variable] -> ShowS
GetRange THF_variable Source #
Methods getRange :: THF_variable -> Range Source # rangeSpan :: THF_variable -> [Pos] Source #

data THF_typed_variable Source #

Constructors

THF_typed_variable Variable THF_top_level_type

Instances

Eq THF_typed_variable Source #
Methods (==) :: THF_typed_variable -> THF_typed_variable -> Bool (/=) :: THF_typed_variable -> THF_typed_variable -> Bool
Data THF_typed_variable Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_typed_variable -> c THF_typed_variable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_typed_variable toConstr :: THF_typed_variable -> Constr dataTypeOf :: THF_typed_variable -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_typed_variable) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_typed_variable) gmapT :: (forall b. Data b => b -> b) -> THF_typed_variable -> THF_typed_variable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_typed_variable -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_typed_variable -> r gmapQ :: (forall d. Data d => d -> u) -> THF_typed_variable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_typed_variable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_typed_variable -> m THF_typed_variable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_typed_variable -> m THF_typed_variable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_typed_variable -> m THF_typed_variable
Ord THF_typed_variable Source #
Methods compare :: THF_typed_variable -> THF_typed_variable -> Ordering (<) :: THF_typed_variable -> THF_typed_variable -> Bool (<=) :: THF_typed_variable -> THF_typed_variable -> Bool (>) :: THF_typed_variable -> THF_typed_variable -> Bool (>=) :: THF_typed_variable -> THF_typed_variable -> Bool max :: THF_typed_variable -> THF_typed_variable -> THF_typed_variable min :: THF_typed_variable -> THF_typed_variable -> THF_typed_variable
Show THF_typed_variable Source #
Methods showsPrec :: Int -> THF_typed_variable -> ShowS show :: THF_typed_variable -> String showList :: [THF_typed_variable] -> ShowS
GetRange THF_typed_variable Source #
Methods getRange :: THF_typed_variable -> Range Source # rangeSpan :: THF_typed_variable -> [Pos] Source #

data THF_unary_formula Source #

Constructors

THF_unary_formula THF_unary_connective THF_logic_formula

Instances

Eq THF_unary_formula Source #
Methods (==) :: THF_unary_formula -> THF_unary_formula -> Bool (/=) :: THF_unary_formula -> THF_unary_formula -> Bool
Data THF_unary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_unary_formula -> c THF_unary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_unary_formula toConstr :: THF_unary_formula -> Constr dataTypeOf :: THF_unary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_unary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_unary_formula) gmapT :: (forall b. Data b => b -> b) -> THF_unary_formula -> THF_unary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_unary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_unary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_unary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_unary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_unary_formula -> m THF_unary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unary_formula -> m THF_unary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unary_formula -> m THF_unary_formula
Ord THF_unary_formula Source #
Methods compare :: THF_unary_formula -> THF_unary_formula -> Ordering (<) :: THF_unary_formula -> THF_unary_formula -> Bool (<=) :: THF_unary_formula -> THF_unary_formula -> Bool (>) :: THF_unary_formula -> THF_unary_formula -> Bool (>=) :: THF_unary_formula -> THF_unary_formula -> Bool max :: THF_unary_formula -> THF_unary_formula -> THF_unary_formula min :: THF_unary_formula -> THF_unary_formula -> THF_unary_formula
Show THF_unary_formula Source #
Methods showsPrec :: Int -> THF_unary_formula -> ShowS show :: THF_unary_formula -> String showList :: [THF_unary_formula] -> ShowS
GetRange THF_unary_formula Source #
Methods getRange :: THF_unary_formula -> Range Source # rangeSpan :: THF_unary_formula -> [Pos] Source #

data THF_atom Source #

Constructors

THF_atom_function THF_function
THF_atom_variable Variable
THF_atom_defined Defined_term
THF_atom_conn THF_conn_term

Instances

Eq THF_atom Source #
Methods (==) :: THF_atom -> THF_atom -> Bool (/=) :: THF_atom -> THF_atom -> Bool
Data THF_atom Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_atom -> c THF_atom gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_atom toConstr :: THF_atom -> Constr dataTypeOf :: THF_atom -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_atom) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_atom) gmapT :: (forall b. Data b => b -> b) -> THF_atom -> THF_atom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_atom -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_atom -> r gmapQ :: (forall d. Data d => d -> u) -> THF_atom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_atom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_atom -> m THF_atom gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_atom -> m THF_atom gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_atom -> m THF_atom
Ord THF_atom Source #
Methods compare :: THF_atom -> THF_atom -> Ordering (<) :: THF_atom -> THF_atom -> Bool (<=) :: THF_atom -> THF_atom -> Bool (>) :: THF_atom -> THF_atom -> Bool (>=) :: THF_atom -> THF_atom -> Bool max :: THF_atom -> THF_atom -> THF_atom min :: THF_atom -> THF_atom -> THF_atom
Show THF_atom Source #
Methods showsPrec :: Int -> THF_atom -> ShowS show :: THF_atom -> String showList :: [THF_atom] -> ShowS
GetRange THF_atom Source #
Methods getRange :: THF_atom -> Range Source # rangeSpan :: THF_atom -> [Pos] Source #

data THF_function Source #

Constructors

THFF_atom Atom
THFF_functor TPTP_functor THF_arguments
THFF_defined Defined_functor THF_arguments
THFF_system System_functor THF_arguments

Instances

Eq THF_function Source #
Methods (==) :: THF_function -> THF_function -> Bool (/=) :: THF_function -> THF_function -> Bool
Data THF_function Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_function -> c THF_function gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_function toConstr :: THF_function -> Constr dataTypeOf :: THF_function -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_function) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_function) gmapT :: (forall b. Data b => b -> b) -> THF_function -> THF_function gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_function -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_function -> r gmapQ :: (forall d. Data d => d -> u) -> THF_function -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_function -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_function -> m THF_function gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_function -> m THF_function gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_function -> m THF_function
Ord THF_function Source #
Methods compare :: THF_function -> THF_function -> Ordering (<) :: THF_function -> THF_function -> Bool (<=) :: THF_function -> THF_function -> Bool (>) :: THF_function -> THF_function -> Bool (>=) :: THF_function -> THF_function -> Bool max :: THF_function -> THF_function -> THF_function min :: THF_function -> THF_function -> THF_function
Show THF_function Source #
Methods showsPrec :: Int -> THF_function -> ShowS show :: THF_function -> String showList :: [THF_function] -> ShowS
GetRange THF_function Source #
Methods getRange :: THF_function -> Range Source # rangeSpan :: THF_function -> [Pos] Source #

data THF_conn_term Source #

Constructors

THFC_pair THF_pair_connective
THFC_assoc Assoc_connective
THFC_unary THF_unary_connective

Instances

Eq THF_conn_term Source #
Methods (==) :: THF_conn_term -> THF_conn_term -> Bool (/=) :: THF_conn_term -> THF_conn_term -> Bool
Data THF_conn_term Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_conn_term -> c THF_conn_term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_conn_term toConstr :: THF_conn_term -> Constr dataTypeOf :: THF_conn_term -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_conn_term) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_conn_term) gmapT :: (forall b. Data b => b -> b) -> THF_conn_term -> THF_conn_term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_conn_term -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_conn_term -> r gmapQ :: (forall d. Data d => d -> u) -> THF_conn_term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_conn_term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_conn_term -> m THF_conn_term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_conn_term -> m THF_conn_term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_conn_term -> m THF_conn_term
Ord THF_conn_term Source #
Methods compare :: THF_conn_term -> THF_conn_term -> Ordering (<) :: THF_conn_term -> THF_conn_term -> Bool (<=) :: THF_conn_term -> THF_conn_term -> Bool (>) :: THF_conn_term -> THF_conn_term -> Bool (>=) :: THF_conn_term -> THF_conn_term -> Bool max :: THF_conn_term -> THF_conn_term -> THF_conn_term min :: THF_conn_term -> THF_conn_term -> THF_conn_term
Show THF_conn_term Source #
Methods showsPrec :: Int -> THF_conn_term -> ShowS show :: THF_conn_term -> String showList :: [THF_conn_term] -> ShowS
GetRange THF_conn_term Source #
Methods getRange :: THF_conn_term -> Range Source # rangeSpan :: THF_conn_term -> [Pos] Source #

data THF_conditional Source #

Constructors

THF_conditional THF_logic_formula THF_logic_formula THF_logic_formula

Instances

Eq THF_conditional Source #
Methods (==) :: THF_conditional -> THF_conditional -> Bool (/=) :: THF_conditional -> THF_conditional -> Bool
Data THF_conditional Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_conditional -> c THF_conditional gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_conditional toConstr :: THF_conditional -> Constr dataTypeOf :: THF_conditional -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_conditional) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_conditional) gmapT :: (forall b. Data b => b -> b) -> THF_conditional -> THF_conditional gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_conditional -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_conditional -> r gmapQ :: (forall d. Data d => d -> u) -> THF_conditional -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_conditional -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_conditional -> m THF_conditional gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_conditional -> m THF_conditional gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_conditional -> m THF_conditional
Ord THF_conditional Source #
Methods compare :: THF_conditional -> THF_conditional -> Ordering (<) :: THF_conditional -> THF_conditional -> Bool (<=) :: THF_conditional -> THF_conditional -> Bool (>) :: THF_conditional -> THF_conditional -> Bool (>=) :: THF_conditional -> THF_conditional -> Bool max :: THF_conditional -> THF_conditional -> THF_conditional min :: THF_conditional -> THF_conditional -> THF_conditional
Show THF_conditional Source #
Methods showsPrec :: Int -> THF_conditional -> ShowS show :: THF_conditional -> String showList :: [THF_conditional] -> ShowS
GetRange THF_conditional Source #
Methods getRange :: THF_conditional -> Range Source # rangeSpan :: THF_conditional -> [Pos] Source #

data THF_let Source #

Constructors

THF_let THF_let_defns THF_formula

Instances

Eq THF_let Source #
Methods (==) :: THF_let -> THF_let -> Bool (/=) :: THF_let -> THF_let -> Bool
Data THF_let Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let -> c THF_let gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let toConstr :: THF_let -> Constr dataTypeOf :: THF_let -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let) gmapT :: (forall b. Data b => b -> b) -> THF_let -> THF_let gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let -> m THF_let gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let -> m THF_let gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let -> m THF_let
Ord THF_let Source #
Methods compare :: THF_let -> THF_let -> Ordering (<) :: THF_let -> THF_let -> Bool (<=) :: THF_let -> THF_let -> Bool (>) :: THF_let -> THF_let -> Bool (>=) :: THF_let -> THF_let -> Bool max :: THF_let -> THF_let -> THF_let min :: THF_let -> THF_let -> THF_let
Show THF_let Source #
Methods showsPrec :: Int -> THF_let -> ShowS show :: THF_let -> String showList :: [THF_let] -> ShowS
GetRange THF_let Source #
Methods getRange :: THF_let -> Range Source # rangeSpan :: THF_let -> [Pos] Source #

data THF_let_defns Source #

Constructors

THFLD_single THF_let_defn
THFLD_many THF_let_defn_list

Instances

Eq THF_let_defns Source #
Methods (==) :: THF_let_defns -> THF_let_defns -> Bool (/=) :: THF_let_defns -> THF_let_defns -> Bool
Data THF_let_defns Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let_defns -> c THF_let_defns gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let_defns toConstr :: THF_let_defns -> Constr dataTypeOf :: THF_let_defns -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let_defns) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let_defns) gmapT :: (forall b. Data b => b -> b) -> THF_let_defns -> THF_let_defns gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defns -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defns -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let_defns -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let_defns -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let_defns -> m THF_let_defns gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defns -> m THF_let_defns gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defns -> m THF_let_defns
Ord THF_let_defns Source #
Methods compare :: THF_let_defns -> THF_let_defns -> Ordering (<) :: THF_let_defns -> THF_let_defns -> Bool (<=) :: THF_let_defns -> THF_let_defns -> Bool (>) :: THF_let_defns -> THF_let_defns -> Bool (>=) :: THF_let_defns -> THF_let_defns -> Bool max :: THF_let_defns -> THF_let_defns -> THF_let_defns min :: THF_let_defns -> THF_let_defns -> THF_let_defns
Show THF_let_defns Source #
Methods showsPrec :: Int -> THF_let_defns -> ShowS show :: THF_let_defns -> String showList :: [THF_let_defns] -> ShowS
GetRange THF_let_defns Source #
Methods getRange :: THF_let_defns -> Range Source # rangeSpan :: THF_let_defns -> [Pos] Source #

type THF_let_defn_list = [THF_let_defn] Source #

data THF_let_defn Source #

Constructors

THFLD_quantified THF_let_quantified_defn
THFLD_plain THF_let_plain_defn

Instances

Eq THF_let_defn Source #
Methods (==) :: THF_let_defn -> THF_let_defn -> Bool (/=) :: THF_let_defn -> THF_let_defn -> Bool
Data THF_let_defn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let_defn -> c THF_let_defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let_defn toConstr :: THF_let_defn -> Constr dataTypeOf :: THF_let_defn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let_defn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let_defn) gmapT :: (forall b. Data b => b -> b) -> THF_let_defn -> THF_let_defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defn -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let_defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let_defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let_defn -> m THF_let_defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defn -> m THF_let_defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defn -> m THF_let_defn
Ord THF_let_defn Source #
Methods compare :: THF_let_defn -> THF_let_defn -> Ordering (<) :: THF_let_defn -> THF_let_defn -> Bool (<=) :: THF_let_defn -> THF_let_defn -> Bool (>) :: THF_let_defn -> THF_let_defn -> Bool (>=) :: THF_let_defn -> THF_let_defn -> Bool max :: THF_let_defn -> THF_let_defn -> THF_let_defn min :: THF_let_defn -> THF_let_defn -> THF_let_defn
Show THF_let_defn Source #
Methods showsPrec :: Int -> THF_let_defn -> ShowS show :: THF_let_defn -> String showList :: [THF_let_defn] -> ShowS
GetRange THF_let_defn Source #
Methods getRange :: THF_let_defn -> Range Source # rangeSpan :: THF_let_defn -> [Pos] Source #

data THF_let_quantified_defn Source #

Constructors

THF_let_quantified_defn THF_quantification THF_let_plain_defn

Instances

Eq THF_let_quantified_defn Source #
Methods (==) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool (/=) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool
Data THF_let_quantified_defn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let_quantified_defn -> c THF_let_quantified_defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let_quantified_defn toConstr :: THF_let_quantified_defn -> Constr dataTypeOf :: THF_let_quantified_defn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let_quantified_defn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let_quantified_defn) gmapT :: (forall b. Data b => b -> b) -> THF_let_quantified_defn -> THF_let_quantified_defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_quantified_defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_quantified_defn -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let_quantified_defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let_quantified_defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let_quantified_defn -> m THF_let_quantified_defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_quantified_defn -> m THF_let_quantified_defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_quantified_defn -> m THF_let_quantified_defn
Ord THF_let_quantified_defn Source #
Methods compare :: THF_let_quantified_defn -> THF_let_quantified_defn -> Ordering (<) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool (<=) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool (>) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool (>=) :: THF_let_quantified_defn -> THF_let_quantified_defn -> Bool max :: THF_let_quantified_defn -> THF_let_quantified_defn -> THF_let_quantified_defn min :: THF_let_quantified_defn -> THF_let_quantified_defn -> THF_let_quantified_defn
Show THF_let_quantified_defn Source #
Methods showsPrec :: Int -> THF_let_quantified_defn -> ShowS show :: THF_let_quantified_defn -> String showList :: [THF_let_quantified_defn] -> ShowS
GetRange THF_let_quantified_defn Source #
Methods getRange :: THF_let_quantified_defn -> Range Source # rangeSpan :: THF_let_quantified_defn -> [Pos] Source #

data THF_let_plain_defn Source #

Constructors

THF_let_plain_defn THF_let_defn_LHS THF_formula

Instances

Eq THF_let_plain_defn Source #
Methods (==) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (/=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool
Data THF_let_plain_defn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let_plain_defn -> c THF_let_plain_defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let_plain_defn toConstr :: THF_let_plain_defn -> Constr dataTypeOf :: THF_let_plain_defn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let_plain_defn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let_plain_defn) gmapT :: (forall b. Data b => b -> b) -> THF_let_plain_defn -> THF_let_plain_defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_plain_defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_plain_defn -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let_plain_defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let_plain_defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let_plain_defn -> m THF_let_plain_defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_plain_defn -> m THF_let_plain_defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_plain_defn -> m THF_let_plain_defn
Ord THF_let_plain_defn Source #
Methods compare :: THF_let_plain_defn -> THF_let_plain_defn -> Ordering (<) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (<=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (>) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (>=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool max :: THF_let_plain_defn -> THF_let_plain_defn -> THF_let_plain_defn min :: THF_let_plain_defn -> THF_let_plain_defn -> THF_let_plain_defn
Show THF_let_plain_defn Source #
Methods showsPrec :: Int -> THF_let_plain_defn -> ShowS show :: THF_let_plain_defn -> String showList :: [THF_let_plain_defn] -> ShowS
GetRange THF_let_plain_defn Source #
Methods getRange :: THF_let_plain_defn -> Range Source # rangeSpan :: THF_let_plain_defn -> [Pos] Source #

data THF_let_defn_LHS Source #

Constructors

THFLDL_constant Constant
THFLDL_functor TPTP_functor FOF_arguments
THFLDL_tuple THF_tuple

Instances

Eq THF_let_defn_LHS Source #
Methods (==) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (/=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool
Data THF_let_defn_LHS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_let_defn_LHS -> c THF_let_defn_LHS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_let_defn_LHS toConstr :: THF_let_defn_LHS -> Constr dataTypeOf :: THF_let_defn_LHS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_let_defn_LHS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_let_defn_LHS) gmapT :: (forall b. Data b => b -> b) -> THF_let_defn_LHS -> THF_let_defn_LHS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defn_LHS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_let_defn_LHS -> r gmapQ :: (forall d. Data d => d -> u) -> THF_let_defn_LHS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_let_defn_LHS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_let_defn_LHS -> m THF_let_defn_LHS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defn_LHS -> m THF_let_defn_LHS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_let_defn_LHS -> m THF_let_defn_LHS
Ord THF_let_defn_LHS Source #
Methods compare :: THF_let_defn_LHS -> THF_let_defn_LHS -> Ordering (<) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (<=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (>) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (>=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool max :: THF_let_defn_LHS -> THF_let_defn_LHS -> THF_let_defn_LHS min :: THF_let_defn_LHS -> THF_let_defn_LHS -> THF_let_defn_LHS
Show THF_let_defn_LHS Source #
Methods showsPrec :: Int -> THF_let_defn_LHS -> ShowS show :: THF_let_defn_LHS -> String showList :: [THF_let_defn_LHS] -> ShowS
GetRange THF_let_defn_LHS Source #
Methods getRange :: THF_let_defn_LHS -> Range Source # rangeSpan :: THF_let_defn_LHS -> [Pos] Source #

type THF_arguments = THF_formula_list Source #

data THF_type_formula Source #

Constructors

THFTF_typeable THF_typeable_formula THF_top_level_type
THFTF_constant Constant THF_top_level_type

Instances

Eq THF_type_formula Source #
Methods (==) :: THF_type_formula -> THF_type_formula -> Bool (/=) :: THF_type_formula -> THF_type_formula -> Bool
Data THF_type_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_type_formula -> c THF_type_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_type_formula toConstr :: THF_type_formula -> Constr dataTypeOf :: THF_type_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_type_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_type_formula) gmapT :: (forall b. Data b => b -> b) -> THF_type_formula -> THF_type_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_type_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_type_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_type_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_type_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_type_formula -> m THF_type_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_type_formula -> m THF_type_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_type_formula -> m THF_type_formula
Ord THF_type_formula Source #
Methods compare :: THF_type_formula -> THF_type_formula -> Ordering (<) :: THF_type_formula -> THF_type_formula -> Bool (<=) :: THF_type_formula -> THF_type_formula -> Bool (>) :: THF_type_formula -> THF_type_formula -> Bool (>=) :: THF_type_formula -> THF_type_formula -> Bool max :: THF_type_formula -> THF_type_formula -> THF_type_formula min :: THF_type_formula -> THF_type_formula -> THF_type_formula
Show THF_type_formula Source #
Methods showsPrec :: Int -> THF_type_formula -> ShowS show :: THF_type_formula -> String showList :: [THF_type_formula] -> ShowS
GetRange THF_type_formula Source #
Methods getRange :: THF_type_formula -> Range Source # rangeSpan :: THF_type_formula -> [Pos] Source #

data THF_typeable_formula Source #

Constructors

THFTF_atom THF_atom
THFTF_logic THF_logic_formula

Instances

Eq THF_typeable_formula Source #
Methods (==) :: THF_typeable_formula -> THF_typeable_formula -> Bool (/=) :: THF_typeable_formula -> THF_typeable_formula -> Bool
Data THF_typeable_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_typeable_formula -> c THF_typeable_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_typeable_formula toConstr :: THF_typeable_formula -> Constr dataTypeOf :: THF_typeable_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_typeable_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_typeable_formula) gmapT :: (forall b. Data b => b -> b) -> THF_typeable_formula -> THF_typeable_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_typeable_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_typeable_formula -> r gmapQ :: (forall d. Data d => d -> u) -> THF_typeable_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_typeable_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_typeable_formula -> m THF_typeable_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_typeable_formula -> m THF_typeable_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_typeable_formula -> m THF_typeable_formula
Ord THF_typeable_formula Source #
Methods compare :: THF_typeable_formula -> THF_typeable_formula -> Ordering (<) :: THF_typeable_formula -> THF_typeable_formula -> Bool (<=) :: THF_typeable_formula -> THF_typeable_formula -> Bool (>) :: THF_typeable_formula -> THF_typeable_formula -> Bool (>=) :: THF_typeable_formula -> THF_typeable_formula -> Bool max :: THF_typeable_formula -> THF_typeable_formula -> THF_typeable_formula min :: THF_typeable_formula -> THF_typeable_formula -> THF_typeable_formula
Show THF_typeable_formula Source #
Methods showsPrec :: Int -> THF_typeable_formula -> ShowS show :: THF_typeable_formula -> String showList :: [THF_typeable_formula] -> ShowS
GetRange THF_typeable_formula Source #
Methods getRange :: THF_typeable_formula -> Range Source # rangeSpan :: THF_typeable_formula -> [Pos] Source #

data THF_subtype Source #

Constructors

THF_subtype THF_atom THF_atom

Instances

Eq THF_subtype Source #
Methods (==) :: THF_subtype -> THF_subtype -> Bool (/=) :: THF_subtype -> THF_subtype -> Bool
Data THF_subtype Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_subtype -> c THF_subtype gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_subtype toConstr :: THF_subtype -> Constr dataTypeOf :: THF_subtype -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_subtype) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_subtype) gmapT :: (forall b. Data b => b -> b) -> THF_subtype -> THF_subtype gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_subtype -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_subtype -> r gmapQ :: (forall d. Data d => d -> u) -> THF_subtype -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_subtype -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_subtype -> m THF_subtype gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_subtype -> m THF_subtype gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_subtype -> m THF_subtype
Ord THF_subtype Source #
Methods compare :: THF_subtype -> THF_subtype -> Ordering (<) :: THF_subtype -> THF_subtype -> Bool (<=) :: THF_subtype -> THF_subtype -> Bool (>) :: THF_subtype -> THF_subtype -> Bool (>=) :: THF_subtype -> THF_subtype -> Bool max :: THF_subtype -> THF_subtype -> THF_subtype min :: THF_subtype -> THF_subtype -> THF_subtype
Show THF_subtype Source #
Methods showsPrec :: Int -> THF_subtype -> ShowS show :: THF_subtype -> String showList :: [THF_subtype] -> ShowS
GetRange THF_subtype Source #
Methods getRange :: THF_subtype -> Range Source # rangeSpan :: THF_subtype -> [Pos] Source #

data THF_top_level_type Source #

Constructors

THFTLT_unitary THF_unitary_type
THFTLT_mapping THF_mapping_type

Instances

Eq THF_top_level_type Source #
Methods (==) :: THF_top_level_type -> THF_top_level_type -> Bool (/=) :: THF_top_level_type -> THF_top_level_type -> Bool
Data THF_top_level_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_top_level_type -> c THF_top_level_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_top_level_type toConstr :: THF_top_level_type -> Constr dataTypeOf :: THF_top_level_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_top_level_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_top_level_type) gmapT :: (forall b. Data b => b -> b) -> THF_top_level_type -> THF_top_level_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_top_level_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_top_level_type -> r gmapQ :: (forall d. Data d => d -> u) -> THF_top_level_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_top_level_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_top_level_type -> m THF_top_level_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_top_level_type -> m THF_top_level_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_top_level_type -> m THF_top_level_type
Ord THF_top_level_type Source #
Methods compare :: THF_top_level_type -> THF_top_level_type -> Ordering (<) :: THF_top_level_type -> THF_top_level_type -> Bool (<=) :: THF_top_level_type -> THF_top_level_type -> Bool (>) :: THF_top_level_type -> THF_top_level_type -> Bool (>=) :: THF_top_level_type -> THF_top_level_type -> Bool max :: THF_top_level_type -> THF_top_level_type -> THF_top_level_type min :: THF_top_level_type -> THF_top_level_type -> THF_top_level_type
Show THF_top_level_type Source #
Methods showsPrec :: Int -> THF_top_level_type -> ShowS show :: THF_top_level_type -> String showList :: [THF_top_level_type] -> ShowS
GetRange THF_top_level_type Source #
Methods getRange :: THF_top_level_type -> Range Source # rangeSpan :: THF_top_level_type -> [Pos] Source #

data THF_unitary_type Source #

Constructors

THFUT_unitary THF_unitary_formula
THFUT_binary THF_binary_type

Instances

Eq THF_unitary_type Source #
Methods (==) :: THF_unitary_type -> THF_unitary_type -> Bool (/=) :: THF_unitary_type -> THF_unitary_type -> Bool
Data THF_unitary_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_unitary_type -> c THF_unitary_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_unitary_type toConstr :: THF_unitary_type -> Constr dataTypeOf :: THF_unitary_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_unitary_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_unitary_type) gmapT :: (forall b. Data b => b -> b) -> THF_unitary_type -> THF_unitary_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_unitary_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_unitary_type -> r gmapQ :: (forall d. Data d => d -> u) -> THF_unitary_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_unitary_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_unitary_type -> m THF_unitary_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unitary_type -> m THF_unitary_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_unitary_type -> m THF_unitary_type
Ord THF_unitary_type Source #
Methods compare :: THF_unitary_type -> THF_unitary_type -> Ordering (<) :: THF_unitary_type -> THF_unitary_type -> Bool (<=) :: THF_unitary_type -> THF_unitary_type -> Bool (>) :: THF_unitary_type -> THF_unitary_type -> Bool (>=) :: THF_unitary_type -> THF_unitary_type -> Bool max :: THF_unitary_type -> THF_unitary_type -> THF_unitary_type min :: THF_unitary_type -> THF_unitary_type -> THF_unitary_type
Show THF_unitary_type Source #
Methods showsPrec :: Int -> THF_unitary_type -> ShowS show :: THF_unitary_type -> String showList :: [THF_unitary_type] -> ShowS
GetRange THF_unitary_type Source #
Methods getRange :: THF_unitary_type -> Range Source # rangeSpan :: THF_unitary_type -> [Pos] Source #

data THF_binary_type Source #

Constructors

THFBT_mapping THF_mapping_type
THFBT_xprod THF_xprod_type
THFBT_union THF_union_type

Instances

Eq THF_binary_type Source #
Methods (==) :: THF_binary_type -> THF_binary_type -> Bool (/=) :: THF_binary_type -> THF_binary_type -> Bool
Data THF_binary_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_binary_type -> c THF_binary_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_binary_type toConstr :: THF_binary_type -> Constr dataTypeOf :: THF_binary_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_binary_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_binary_type) gmapT :: (forall b. Data b => b -> b) -> THF_binary_type -> THF_binary_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_binary_type -> r gmapQ :: (forall d. Data d => d -> u) -> THF_binary_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_binary_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_binary_type -> m THF_binary_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_type -> m THF_binary_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_binary_type -> m THF_binary_type
Ord THF_binary_type Source #
Methods compare :: THF_binary_type -> THF_binary_type -> Ordering (<) :: THF_binary_type -> THF_binary_type -> Bool (<=) :: THF_binary_type -> THF_binary_type -> Bool (>) :: THF_binary_type -> THF_binary_type -> Bool (>=) :: THF_binary_type -> THF_binary_type -> Bool max :: THF_binary_type -> THF_binary_type -> THF_binary_type min :: THF_binary_type -> THF_binary_type -> THF_binary_type
Show THF_binary_type Source #
Methods showsPrec :: Int -> THF_binary_type -> ShowS show :: THF_binary_type -> String showList :: [THF_binary_type] -> ShowS
GetRange THF_binary_type Source #
Methods getRange :: THF_binary_type -> Range Source # rangeSpan :: THF_binary_type -> [Pos] Source #

type THF_mapping_type = [THF_unitary_type] Source #

type THF_xprod_type = [THF_unitary_type] Source #

type THF_union_type = [THF_unitary_type] Source #

data THF_sequent Source #

Constructors

THFS_plain THF_tuple THF_tuple
THFS_parens THF_sequent

Instances

Eq THF_sequent Source #
Methods (==) :: THF_sequent -> THF_sequent -> Bool (/=) :: THF_sequent -> THF_sequent -> Bool
Data THF_sequent Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_sequent -> c THF_sequent gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_sequent toConstr :: THF_sequent -> Constr dataTypeOf :: THF_sequent -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_sequent) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_sequent) gmapT :: (forall b. Data b => b -> b) -> THF_sequent -> THF_sequent gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_sequent -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_sequent -> r gmapQ :: (forall d. Data d => d -> u) -> THF_sequent -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_sequent -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_sequent -> m THF_sequent gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_sequent -> m THF_sequent gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_sequent -> m THF_sequent
Ord THF_sequent Source #
Methods compare :: THF_sequent -> THF_sequent -> Ordering (<) :: THF_sequent -> THF_sequent -> Bool (<=) :: THF_sequent -> THF_sequent -> Bool (>) :: THF_sequent -> THF_sequent -> Bool (>=) :: THF_sequent -> THF_sequent -> Bool max :: THF_sequent -> THF_sequent -> THF_sequent min :: THF_sequent -> THF_sequent -> THF_sequent
Show THF_sequent Source #
Methods showsPrec :: Int -> THF_sequent -> ShowS show :: THF_sequent -> String showList :: [THF_sequent] -> ShowS
GetRange THF_sequent Source #
Methods getRange :: THF_sequent -> Range Source # rangeSpan :: THF_sequent -> [Pos] Source #

newtype THF_tuple Source #

Constructors

THF_tuple THF_formula_list

Instances

Eq THF_tuple Source #
Methods (==) :: THF_tuple -> THF_tuple -> Bool (/=) :: THF_tuple -> THF_tuple -> Bool
Data THF_tuple Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THF_tuple -> c THF_tuple gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THF_tuple toConstr :: THF_tuple -> Constr dataTypeOf :: THF_tuple -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c THF_tuple) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THF_tuple) gmapT :: (forall b. Data b => b -> b) -> THF_tuple -> THF_tuple gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THF_tuple -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THF_tuple -> r gmapQ :: (forall d. Data d => d -> u) -> THF_tuple -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THF_tuple -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THF_tuple -> m THF_tuple gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_tuple -> m THF_tuple gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THF_tuple -> m THF_tuple
Ord THF_tuple Source #
Methods compare :: THF_tuple -> THF_tuple -> Ordering (<) :: THF_tuple -> THF_tuple -> Bool (<=) :: THF_tuple -> THF_tuple -> Bool (>) :: THF_tuple -> THF_tuple -> Bool (>=) :: THF_tuple -> THF_tuple -> Bool max :: THF_tuple -> THF_tuple -> THF_tuple min :: THF_tuple -> THF_tuple -> THF_tuple
Show THF_tuple Source #
Methods showsPrec :: Int -> THF_tuple -> ShowS show :: THF_tuple -> String showList :: [THF_tuple] -> ShowS
GetRange THF_tuple Source #
Methods getRange :: THF_tuple -> Range Source # rangeSpan :: THF_tuple -> [Pos] Source #

type THF_formula_list = [THF_logic_formula] Source #

data TFX_formula Source #

Constructors

TFXF_logic TFX_logic_formula
TFXF_sequent THF_sequent

Instances

Eq TFX_formula Source #
Methods (==) :: TFX_formula -> TFX_formula -> Bool (/=) :: TFX_formula -> TFX_formula -> Bool
Data TFX_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFX_formula -> c TFX_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFX_formula toConstr :: TFX_formula -> Constr dataTypeOf :: TFX_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFX_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFX_formula) gmapT :: (forall b. Data b => b -> b) -> TFX_formula -> TFX_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFX_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFX_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFX_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFX_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFX_formula -> m TFX_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_formula -> m TFX_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_formula -> m TFX_formula
Ord TFX_formula Source #
Methods compare :: TFX_formula -> TFX_formula -> Ordering (<) :: TFX_formula -> TFX_formula -> Bool (<=) :: TFX_formula -> TFX_formula -> Bool (>) :: TFX_formula -> TFX_formula -> Bool (>=) :: TFX_formula -> TFX_formula -> Bool max :: TFX_formula -> TFX_formula -> TFX_formula min :: TFX_formula -> TFX_formula -> TFX_formula
Show TFX_formula Source #
Methods showsPrec :: Int -> TFX_formula -> ShowS show :: TFX_formula -> String showList :: [TFX_formula] -> ShowS
GetRange TFX_formula Source #
Methods getRange :: TFX_formula -> Range Source # rangeSpan :: TFX_formula -> [Pos] Source #

data TFX_logic_formula Source #

Constructors

TFXLF_binary THF_binary_formula
TFXLF_unitary THF_unitary_formula
TFXLF_typed TFF_typed_atom
TFXLF_subtype TFF_subtype

Instances

Eq TFX_logic_formula Source #
Methods (==) :: TFX_logic_formula -> TFX_logic_formula -> Bool (/=) :: TFX_logic_formula -> TFX_logic_formula -> Bool
Data TFX_logic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFX_logic_formula -> c TFX_logic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFX_logic_formula toConstr :: TFX_logic_formula -> Constr dataTypeOf :: TFX_logic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFX_logic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFX_logic_formula) gmapT :: (forall b. Data b => b -> b) -> TFX_logic_formula -> TFX_logic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFX_logic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFX_logic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFX_logic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFX_logic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFX_logic_formula -> m TFX_logic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_logic_formula -> m TFX_logic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFX_logic_formula -> m TFX_logic_formula
Ord TFX_logic_formula Source #
Methods compare :: TFX_logic_formula -> TFX_logic_formula -> Ordering (<) :: TFX_logic_formula -> TFX_logic_formula -> Bool (<=) :: TFX_logic_formula -> TFX_logic_formula -> Bool (>) :: TFX_logic_formula -> TFX_logic_formula -> Bool (>=) :: TFX_logic_formula -> TFX_logic_formula -> Bool max :: TFX_logic_formula -> TFX_logic_formula -> TFX_logic_formula min :: TFX_logic_formula -> TFX_logic_formula -> TFX_logic_formula
Show TFX_logic_formula Source #
Methods showsPrec :: Int -> TFX_logic_formula -> ShowS show :: TFX_logic_formula -> String showList :: [TFX_logic_formula] -> ShowS
GetRange TFX_logic_formula Source #
Methods getRange :: TFX_logic_formula -> Range Source # rangeSpan :: TFX_logic_formula -> [Pos] Source #

data TFF_formula Source #

Constructors

TFFF_logic TFF_logic_formula
TFFF_atom TFF_typed_atom
TFFF_sequent TFF_sequent

Instances

Eq TFF_formula Source #
Methods (==) :: TFF_formula -> TFF_formula -> Bool (/=) :: TFF_formula -> TFF_formula -> Bool
Data TFF_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_formula -> c TFF_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_formula toConstr :: TFF_formula -> Constr dataTypeOf :: TFF_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_formula -> TFF_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_formula -> m TFF_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_formula -> m TFF_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_formula -> m TFF_formula
Ord TFF_formula Source #
Methods compare :: TFF_formula -> TFF_formula -> Ordering (<) :: TFF_formula -> TFF_formula -> Bool (<=) :: TFF_formula -> TFF_formula -> Bool (>) :: TFF_formula -> TFF_formula -> Bool (>=) :: TFF_formula -> TFF_formula -> Bool max :: TFF_formula -> TFF_formula -> TFF_formula min :: TFF_formula -> TFF_formula -> TFF_formula
Show TFF_formula Source #
Methods showsPrec :: Int -> TFF_formula -> ShowS show :: TFF_formula -> String showList :: [TFF_formula] -> ShowS
GetRange TFF_formula Source #
Methods getRange :: TFF_formula -> Range Source # rangeSpan :: TFF_formula -> [Pos] Source #

data TFF_logic_formula Source #

Constructors

TFFLF_binary TFF_binary_formula
TFFLF_unitary TFF_unitary_formula
TFFLF_subtype TFF_subtype

Instances

Eq TFF_logic_formula Source #
Methods (==) :: TFF_logic_formula -> TFF_logic_formula -> Bool (/=) :: TFF_logic_formula -> TFF_logic_formula -> Bool
Data TFF_logic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_logic_formula -> c TFF_logic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_logic_formula toConstr :: TFF_logic_formula -> Constr dataTypeOf :: TFF_logic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_logic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_logic_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_logic_formula -> TFF_logic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_logic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_logic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_logic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_logic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_logic_formula -> m TFF_logic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_logic_formula -> m TFF_logic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_logic_formula -> m TFF_logic_formula
Ord TFF_logic_formula Source #
Methods compare :: TFF_logic_formula -> TFF_logic_formula -> Ordering (<) :: TFF_logic_formula -> TFF_logic_formula -> Bool (<=) :: TFF_logic_formula -> TFF_logic_formula -> Bool (>) :: TFF_logic_formula -> TFF_logic_formula -> Bool (>=) :: TFF_logic_formula -> TFF_logic_formula -> Bool max :: TFF_logic_formula -> TFF_logic_formula -> TFF_logic_formula min :: TFF_logic_formula -> TFF_logic_formula -> TFF_logic_formula
Show TFF_logic_formula Source #
Methods showsPrec :: Int -> TFF_logic_formula -> ShowS show :: TFF_logic_formula -> String showList :: [TFF_logic_formula] -> ShowS
GetRange TFF_logic_formula Source #
Methods getRange :: TFF_logic_formula -> Range Source # rangeSpan :: TFF_logic_formula -> [Pos] Source #

data TFF_binary_formula Source #

Constructors

TFFBF_nonassoc TFF_binary_nonassoc
TFFBF_assoc TFF_binary_assoc

Instances

Eq TFF_binary_formula Source #
Methods (==) :: TFF_binary_formula -> TFF_binary_formula -> Bool (/=) :: TFF_binary_formula -> TFF_binary_formula -> Bool
Data TFF_binary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_binary_formula -> c TFF_binary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_binary_formula toConstr :: TFF_binary_formula -> Constr dataTypeOf :: TFF_binary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_binary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_binary_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_binary_formula -> TFF_binary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_binary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_binary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_binary_formula -> m TFF_binary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_formula -> m TFF_binary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_formula -> m TFF_binary_formula
Ord TFF_binary_formula Source #
Methods compare :: TFF_binary_formula -> TFF_binary_formula -> Ordering (<) :: TFF_binary_formula -> TFF_binary_formula -> Bool (<=) :: TFF_binary_formula -> TFF_binary_formula -> Bool (>) :: TFF_binary_formula -> TFF_binary_formula -> Bool (>=) :: TFF_binary_formula -> TFF_binary_formula -> Bool max :: TFF_binary_formula -> TFF_binary_formula -> TFF_binary_formula min :: TFF_binary_formula -> TFF_binary_formula -> TFF_binary_formula
Show TFF_binary_formula Source #
Methods showsPrec :: Int -> TFF_binary_formula -> ShowS show :: TFF_binary_formula -> String showList :: [TFF_binary_formula] -> ShowS
GetRange TFF_binary_formula Source #
Methods getRange :: TFF_binary_formula -> Range Source # rangeSpan :: TFF_binary_formula -> [Pos] Source #

data TFF_binary_nonassoc Source #

Constructors

TFF_binary_nonassoc Binary_connective TFF_unitary_formula TFF_unitary_formula

Instances

Eq TFF_binary_nonassoc Source #
Methods (==) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (/=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool
Data TFF_binary_nonassoc Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_binary_nonassoc -> c TFF_binary_nonassoc gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_binary_nonassoc toConstr :: TFF_binary_nonassoc -> Constr dataTypeOf :: TFF_binary_nonassoc -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_binary_nonassoc) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_binary_nonassoc) gmapT :: (forall b. Data b => b -> b) -> TFF_binary_nonassoc -> TFF_binary_nonassoc gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_nonassoc -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_nonassoc -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_binary_nonassoc -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_binary_nonassoc -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_binary_nonassoc -> m TFF_binary_nonassoc gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_nonassoc -> m TFF_binary_nonassoc gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_nonassoc -> m TFF_binary_nonassoc
Ord TFF_binary_nonassoc Source #
Methods compare :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Ordering (<) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (<=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (>) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (>=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool max :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> TFF_binary_nonassoc min :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> TFF_binary_nonassoc
Show TFF_binary_nonassoc Source #
Methods showsPrec :: Int -> TFF_binary_nonassoc -> ShowS show :: TFF_binary_nonassoc -> String showList :: [TFF_binary_nonassoc] -> ShowS
GetRange TFF_binary_nonassoc Source #
Methods getRange :: TFF_binary_nonassoc -> Range Source # rangeSpan :: TFF_binary_nonassoc -> [Pos] Source #

data TFF_binary_assoc Source #

Constructors

TFFBA_or TFF_or_formula
TFFBA_and TFF_and_formula

Instances

Eq TFF_binary_assoc Source #
Methods (==) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool (/=) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool
Data TFF_binary_assoc Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_binary_assoc -> c TFF_binary_assoc gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_binary_assoc toConstr :: TFF_binary_assoc -> Constr dataTypeOf :: TFF_binary_assoc -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_binary_assoc) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_binary_assoc) gmapT :: (forall b. Data b => b -> b) -> TFF_binary_assoc -> TFF_binary_assoc gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_assoc -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_binary_assoc -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_binary_assoc -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_binary_assoc -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_binary_assoc -> m TFF_binary_assoc gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_assoc -> m TFF_binary_assoc gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_binary_assoc -> m TFF_binary_assoc
Ord TFF_binary_assoc Source #
Methods compare :: TFF_binary_assoc -> TFF_binary_assoc -> Ordering (<) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool (<=) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool (>) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool (>=) :: TFF_binary_assoc -> TFF_binary_assoc -> Bool max :: TFF_binary_assoc -> TFF_binary_assoc -> TFF_binary_assoc min :: TFF_binary_assoc -> TFF_binary_assoc -> TFF_binary_assoc
Show TFF_binary_assoc Source #
Methods showsPrec :: Int -> TFF_binary_assoc -> ShowS show :: TFF_binary_assoc -> String showList :: [TFF_binary_assoc] -> ShowS
GetRange TFF_binary_assoc Source #
Methods getRange :: TFF_binary_assoc -> Range Source # rangeSpan :: TFF_binary_assoc -> [Pos] Source #

type TFF_or_formula = [TFF_unitary_formula] Source #

type TFF_and_formula = [TFF_unitary_formula] Source #

data TFF_unitary_formula Source #

Constructors

TFFUF_quantified TFF_quantified_formula
TFFUF_unary TFF_unary_formula
TFFUF_atomic TFF_atomic_formula
TFFUF_conditional TFF_conditional
TFFUF_let TFF_let
TFFUF_logic TFF_logic_formula

Instances

Eq TFF_unitary_formula Source #
Methods (==) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool (/=) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool
Data TFF_unitary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_unitary_formula -> c TFF_unitary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_unitary_formula toConstr :: TFF_unitary_formula -> Constr dataTypeOf :: TFF_unitary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_unitary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_unitary_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_unitary_formula -> TFF_unitary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unitary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unitary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_unitary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_unitary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_unitary_formula -> m TFF_unitary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unitary_formula -> m TFF_unitary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unitary_formula -> m TFF_unitary_formula
Ord TFF_unitary_formula Source #
Methods compare :: TFF_unitary_formula -> TFF_unitary_formula -> Ordering (<) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool (<=) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool (>) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool (>=) :: TFF_unitary_formula -> TFF_unitary_formula -> Bool max :: TFF_unitary_formula -> TFF_unitary_formula -> TFF_unitary_formula min :: TFF_unitary_formula -> TFF_unitary_formula -> TFF_unitary_formula
Show TFF_unitary_formula Source #
Methods showsPrec :: Int -> TFF_unitary_formula -> ShowS show :: TFF_unitary_formula -> String showList :: [TFF_unitary_formula] -> ShowS
GetRange TFF_unitary_formula Source #
Methods getRange :: TFF_unitary_formula -> Range Source # rangeSpan :: TFF_unitary_formula -> [Pos] Source #

data TFF_quantified_formula Source #

Constructors

TFF_quantified_formula FOF_quantifier TFF_variable_list TFF_unitary_formula

Instances

Eq TFF_quantified_formula Source #
Methods (==) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool (/=) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool
Data TFF_quantified_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_quantified_formula -> c TFF_quantified_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_quantified_formula toConstr :: TFF_quantified_formula -> Constr dataTypeOf :: TFF_quantified_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_quantified_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_quantified_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_quantified_formula -> TFF_quantified_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_quantified_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_quantified_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_quantified_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_quantified_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_quantified_formula -> m TFF_quantified_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_quantified_formula -> m TFF_quantified_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_quantified_formula -> m TFF_quantified_formula
Ord TFF_quantified_formula Source #
Methods compare :: TFF_quantified_formula -> TFF_quantified_formula -> Ordering (<) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool (<=) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool (>) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool (>=) :: TFF_quantified_formula -> TFF_quantified_formula -> Bool max :: TFF_quantified_formula -> TFF_quantified_formula -> TFF_quantified_formula min :: TFF_quantified_formula -> TFF_quantified_formula -> TFF_quantified_formula
Show TFF_quantified_formula Source #
Methods showsPrec :: Int -> TFF_quantified_formula -> ShowS show :: TFF_quantified_formula -> String showList :: [TFF_quantified_formula] -> ShowS
GetRange TFF_quantified_formula Source #
Methods getRange :: TFF_quantified_formula -> Range Source # rangeSpan :: TFF_quantified_formula -> [Pos] Source #

type TFF_variable_list = [TFF_variable] Source #

data TFF_variable Source #

Constructors

TFFV_typed TFF_typed_variable
TFFV_variable Variable

Instances

Eq TFF_variable Source #
Methods (==) :: TFF_variable -> TFF_variable -> Bool (/=) :: TFF_variable -> TFF_variable -> Bool
Data TFF_variable Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_variable -> c TFF_variable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_variable toConstr :: TFF_variable -> Constr dataTypeOf :: TFF_variable -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_variable) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_variable) gmapT :: (forall b. Data b => b -> b) -> TFF_variable -> TFF_variable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_variable -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_variable -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_variable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_variable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_variable -> m TFF_variable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_variable -> m TFF_variable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_variable -> m TFF_variable
Ord TFF_variable Source #
Methods compare :: TFF_variable -> TFF_variable -> Ordering (<) :: TFF_variable -> TFF_variable -> Bool (<=) :: TFF_variable -> TFF_variable -> Bool (>) :: TFF_variable -> TFF_variable -> Bool (>=) :: TFF_variable -> TFF_variable -> Bool max :: TFF_variable -> TFF_variable -> TFF_variable min :: TFF_variable -> TFF_variable -> TFF_variable
Show TFF_variable Source #
Methods showsPrec :: Int -> TFF_variable -> ShowS show :: TFF_variable -> String showList :: [TFF_variable] -> ShowS
GetRange TFF_variable Source #
Methods getRange :: TFF_variable -> Range Source # rangeSpan :: TFF_variable -> [Pos] Source #

data TFF_typed_variable Source #

Constructors

TFF_typed_variable Variable TFF_atomic_type

Instances

Eq TFF_typed_variable Source #
Methods (==) :: TFF_typed_variable -> TFF_typed_variable -> Bool (/=) :: TFF_typed_variable -> TFF_typed_variable -> Bool
Data TFF_typed_variable Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_typed_variable -> c TFF_typed_variable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_typed_variable toConstr :: TFF_typed_variable -> Constr dataTypeOf :: TFF_typed_variable -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_typed_variable) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_typed_variable) gmapT :: (forall b. Data b => b -> b) -> TFF_typed_variable -> TFF_typed_variable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_typed_variable -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_typed_variable -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_typed_variable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_typed_variable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_typed_variable -> m TFF_typed_variable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_typed_variable -> m TFF_typed_variable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_typed_variable -> m TFF_typed_variable
Ord TFF_typed_variable Source #
Methods compare :: TFF_typed_variable -> TFF_typed_variable -> Ordering (<) :: TFF_typed_variable -> TFF_typed_variable -> Bool (<=) :: TFF_typed_variable -> TFF_typed_variable -> Bool (>) :: TFF_typed_variable -> TFF_typed_variable -> Bool (>=) :: TFF_typed_variable -> TFF_typed_variable -> Bool max :: TFF_typed_variable -> TFF_typed_variable -> TFF_typed_variable min :: TFF_typed_variable -> TFF_typed_variable -> TFF_typed_variable
Show TFF_typed_variable Source #
Methods showsPrec :: Int -> TFF_typed_variable -> ShowS show :: TFF_typed_variable -> String showList :: [TFF_typed_variable] -> ShowS
GetRange TFF_typed_variable Source #
Methods getRange :: TFF_typed_variable -> Range Source # rangeSpan :: TFF_typed_variable -> [Pos] Source #

data TFF_unary_formula Source #

Constructors

TFFUF_connective Unary_connective TFF_unitary_formula
TFFUF_infix FOF_infix_unary

Instances

Eq TFF_unary_formula Source #
Methods (==) :: TFF_unary_formula -> TFF_unary_formula -> Bool (/=) :: TFF_unary_formula -> TFF_unary_formula -> Bool
Data TFF_unary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_unary_formula -> c TFF_unary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_unary_formula toConstr :: TFF_unary_formula -> Constr dataTypeOf :: TFF_unary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_unary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_unary_formula) gmapT :: (forall b. Data b => b -> b) -> TFF_unary_formula -> TFF_unary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_unary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_unary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_unary_formula -> m TFF_unary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unary_formula -> m TFF_unary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unary_formula -> m TFF_unary_formula
Ord TFF_unary_formula Source #
Methods compare :: TFF_unary_formula -> TFF_unary_formula -> Ordering (<) :: TFF_unary_formula -> TFF_unary_formula -> Bool (<=) :: TFF_unary_formula -> TFF_unary_formula -> Bool (>) :: TFF_unary_formula -> TFF_unary_formula -> Bool (>=) :: TFF_unary_formula -> TFF_unary_formula -> Bool max :: TFF_unary_formula -> TFF_unary_formula -> TFF_unary_formula min :: TFF_unary_formula -> TFF_unary_formula -> TFF_unary_formula
Show TFF_unary_formula Source #
Methods showsPrec :: Int -> TFF_unary_formula -> ShowS show :: TFF_unary_formula -> String showList :: [TFF_unary_formula] -> ShowS
GetRange TFF_unary_formula Source #
Methods getRange :: TFF_unary_formula -> Range Source # rangeSpan :: TFF_unary_formula -> [Pos] Source #

type TFF_atomic_formula = FOF_atomic_formula Source #

data TFF_conditional Source #

Constructors

TFF_conditional TFF_logic_formula TFF_logic_formula TFF_logic_formula

Instances

Eq TFF_conditional Source #
Methods (==) :: TFF_conditional -> TFF_conditional -> Bool (/=) :: TFF_conditional -> TFF_conditional -> Bool
Data TFF_conditional Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_conditional -> c TFF_conditional gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_conditional toConstr :: TFF_conditional -> Constr dataTypeOf :: TFF_conditional -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_conditional) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_conditional) gmapT :: (forall b. Data b => b -> b) -> TFF_conditional -> TFF_conditional gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_conditional -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_conditional -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_conditional -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_conditional -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_conditional -> m TFF_conditional gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_conditional -> m TFF_conditional gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_conditional -> m TFF_conditional
Ord TFF_conditional Source #
Methods compare :: TFF_conditional -> TFF_conditional -> Ordering (<) :: TFF_conditional -> TFF_conditional -> Bool (<=) :: TFF_conditional -> TFF_conditional -> Bool (>) :: TFF_conditional -> TFF_conditional -> Bool (>=) :: TFF_conditional -> TFF_conditional -> Bool max :: TFF_conditional -> TFF_conditional -> TFF_conditional min :: TFF_conditional -> TFF_conditional -> TFF_conditional
Show TFF_conditional Source #
Methods showsPrec :: Int -> TFF_conditional -> ShowS show :: TFF_conditional -> String showList :: [TFF_conditional] -> ShowS
GetRange TFF_conditional Source #
Methods getRange :: TFF_conditional -> Range Source # rangeSpan :: TFF_conditional -> [Pos] Source #

data TFF_let Source #

Constructors

TFF_let_term_defns TFF_let_term_defns TFF_formula
TFF_let_formula_defns TFF_let_formula_defns TFF_formula

Instances

Eq TFF_let Source #
Methods (==) :: TFF_let -> TFF_let -> Bool (/=) :: TFF_let -> TFF_let -> Bool
Data TFF_let Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let -> c TFF_let gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let toConstr :: TFF_let -> Constr dataTypeOf :: TFF_let -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let) gmapT :: (forall b. Data b => b -> b) -> TFF_let -> TFF_let gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let -> m TFF_let gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let -> m TFF_let gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let -> m TFF_let
Ord TFF_let Source #
Methods compare :: TFF_let -> TFF_let -> Ordering (<) :: TFF_let -> TFF_let -> Bool (<=) :: TFF_let -> TFF_let -> Bool (>) :: TFF_let -> TFF_let -> Bool (>=) :: TFF_let -> TFF_let -> Bool max :: TFF_let -> TFF_let -> TFF_let min :: TFF_let -> TFF_let -> TFF_let
Show TFF_let Source #
Methods showsPrec :: Int -> TFF_let -> ShowS show :: TFF_let -> String showList :: [TFF_let] -> ShowS
GetRange TFF_let Source #
Methods getRange :: TFF_let -> Range Source # rangeSpan :: TFF_let -> [Pos] Source #

data TFF_let_term_defns Source #

Constructors

TFFLTD_single TFF_let_term_defn
TFFLTD_many TFF_let_term_list

Instances

Eq TFF_let_term_defns Source #
Methods (==) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool (/=) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool
Data TFF_let_term_defns Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_term_defns -> c TFF_let_term_defns gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_term_defns toConstr :: TFF_let_term_defns -> Constr dataTypeOf :: TFF_let_term_defns -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_term_defns) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_term_defns) gmapT :: (forall b. Data b => b -> b) -> TFF_let_term_defns -> TFF_let_term_defns gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_defns -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_defns -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_term_defns -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_term_defns -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_term_defns -> m TFF_let_term_defns gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_defns -> m TFF_let_term_defns gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_defns -> m TFF_let_term_defns
Ord TFF_let_term_defns Source #
Methods compare :: TFF_let_term_defns -> TFF_let_term_defns -> Ordering (<) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool (<=) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool (>) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool (>=) :: TFF_let_term_defns -> TFF_let_term_defns -> Bool max :: TFF_let_term_defns -> TFF_let_term_defns -> TFF_let_term_defns min :: TFF_let_term_defns -> TFF_let_term_defns -> TFF_let_term_defns
Show TFF_let_term_defns Source #
Methods showsPrec :: Int -> TFF_let_term_defns -> ShowS show :: TFF_let_term_defns -> String showList :: [TFF_let_term_defns] -> ShowS
GetRange TFF_let_term_defns Source #
Methods getRange :: TFF_let_term_defns -> Range Source # rangeSpan :: TFF_let_term_defns -> [Pos] Source #

type TFF_let_term_list = [TFF_let_term_defn] Source #

data TFF_let_term_defn Source #

Constructors

TFFLTD_variable TFF_variable_list TFF_let_term_defn
TFFLTD_binding TFF_let_term_binding

Instances

Eq TFF_let_term_defn Source #
Methods (==) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool (/=) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool
Data TFF_let_term_defn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_term_defn -> c TFF_let_term_defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_term_defn toConstr :: TFF_let_term_defn -> Constr dataTypeOf :: TFF_let_term_defn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_term_defn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_term_defn) gmapT :: (forall b. Data b => b -> b) -> TFF_let_term_defn -> TFF_let_term_defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_defn -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_term_defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_term_defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_term_defn -> m TFF_let_term_defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_defn -> m TFF_let_term_defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_defn -> m TFF_let_term_defn
Ord TFF_let_term_defn Source #
Methods compare :: TFF_let_term_defn -> TFF_let_term_defn -> Ordering (<) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool (<=) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool (>) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool (>=) :: TFF_let_term_defn -> TFF_let_term_defn -> Bool max :: TFF_let_term_defn -> TFF_let_term_defn -> TFF_let_term_defn min :: TFF_let_term_defn -> TFF_let_term_defn -> TFF_let_term_defn
Show TFF_let_term_defn Source #
Methods showsPrec :: Int -> TFF_let_term_defn -> ShowS show :: TFF_let_term_defn -> String showList :: [TFF_let_term_defn] -> ShowS
GetRange TFF_let_term_defn Source #
Methods getRange :: TFF_let_term_defn -> Range Source # rangeSpan :: TFF_let_term_defn -> [Pos] Source #

data TFF_let_term_binding Source #

Constructors

TFFLTB_plain FOF_plain_term FOF_term
TFFLTB_binding TFF_let_term_binding

Instances

Eq TFF_let_term_binding Source #
Methods (==) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool (/=) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool
Data TFF_let_term_binding Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_term_binding -> c TFF_let_term_binding gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_term_binding toConstr :: TFF_let_term_binding -> Constr dataTypeOf :: TFF_let_term_binding -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_term_binding) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_term_binding) gmapT :: (forall b. Data b => b -> b) -> TFF_let_term_binding -> TFF_let_term_binding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_binding -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_term_binding -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_term_binding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_term_binding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_term_binding -> m TFF_let_term_binding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_binding -> m TFF_let_term_binding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_term_binding -> m TFF_let_term_binding
Ord TFF_let_term_binding Source #
Methods compare :: TFF_let_term_binding -> TFF_let_term_binding -> Ordering (<) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool (<=) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool (>) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool (>=) :: TFF_let_term_binding -> TFF_let_term_binding -> Bool max :: TFF_let_term_binding -> TFF_let_term_binding -> TFF_let_term_binding min :: TFF_let_term_binding -> TFF_let_term_binding -> TFF_let_term_binding
Show TFF_let_term_binding Source #
Methods showsPrec :: Int -> TFF_let_term_binding -> ShowS show :: TFF_let_term_binding -> String showList :: [TFF_let_term_binding] -> ShowS
GetRange TFF_let_term_binding Source #
Methods getRange :: TFF_let_term_binding -> Range Source # rangeSpan :: TFF_let_term_binding -> [Pos] Source #

data TFF_let_formula_defns Source #

Constructors

TFFLFD_single TFF_let_formula_defn
TFFLFD_many TFF_let_formula_list

Instances

Eq TFF_let_formula_defns Source #
Methods (==) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool (/=) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool
Data TFF_let_formula_defns Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_formula_defns -> c TFF_let_formula_defns gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_formula_defns toConstr :: TFF_let_formula_defns -> Constr dataTypeOf :: TFF_let_formula_defns -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_formula_defns) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_formula_defns) gmapT :: (forall b. Data b => b -> b) -> TFF_let_formula_defns -> TFF_let_formula_defns gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_defns -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_defns -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_formula_defns -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_formula_defns -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_formula_defns -> m TFF_let_formula_defns gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_defns -> m TFF_let_formula_defns gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_defns -> m TFF_let_formula_defns
Ord TFF_let_formula_defns Source #
Methods compare :: TFF_let_formula_defns -> TFF_let_formula_defns -> Ordering (<) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool (<=) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool (>) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool (>=) :: TFF_let_formula_defns -> TFF_let_formula_defns -> Bool max :: TFF_let_formula_defns -> TFF_let_formula_defns -> TFF_let_formula_defns min :: TFF_let_formula_defns -> TFF_let_formula_defns -> TFF_let_formula_defns
Show TFF_let_formula_defns Source #
Methods showsPrec :: Int -> TFF_let_formula_defns -> ShowS show :: TFF_let_formula_defns -> String showList :: [TFF_let_formula_defns] -> ShowS
GetRange TFF_let_formula_defns Source #
Methods getRange :: TFF_let_formula_defns -> Range Source # rangeSpan :: TFF_let_formula_defns -> [Pos] Source #

type TFF_let_formula_list = [TFF_let_formula_defn] Source #

data TFF_let_formula_defn Source #

Constructors

TFFLFD_variable TFF_variable_list TFF_let_formula_defn
TFFLFD_binding TFF_let_formula_binding

Instances

Eq TFF_let_formula_defn Source #
Methods (==) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool (/=) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool
Data TFF_let_formula_defn Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_formula_defn -> c TFF_let_formula_defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_formula_defn toConstr :: TFF_let_formula_defn -> Constr dataTypeOf :: TFF_let_formula_defn -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_formula_defn) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_formula_defn) gmapT :: (forall b. Data b => b -> b) -> TFF_let_formula_defn -> TFF_let_formula_defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_defn -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_formula_defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_formula_defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_formula_defn -> m TFF_let_formula_defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_defn -> m TFF_let_formula_defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_defn -> m TFF_let_formula_defn
Ord TFF_let_formula_defn Source #
Methods compare :: TFF_let_formula_defn -> TFF_let_formula_defn -> Ordering (<) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool (<=) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool (>) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool (>=) :: TFF_let_formula_defn -> TFF_let_formula_defn -> Bool max :: TFF_let_formula_defn -> TFF_let_formula_defn -> TFF_let_formula_defn min :: TFF_let_formula_defn -> TFF_let_formula_defn -> TFF_let_formula_defn
Show TFF_let_formula_defn Source #
Methods showsPrec :: Int -> TFF_let_formula_defn -> ShowS show :: TFF_let_formula_defn -> String showList :: [TFF_let_formula_defn] -> ShowS
GetRange TFF_let_formula_defn Source #
Methods getRange :: TFF_let_formula_defn -> Range Source # rangeSpan :: TFF_let_formula_defn -> [Pos] Source #

data TFF_let_formula_binding Source #

Constructors

TFFLFB_plain FOF_plain_atomic_formula TFF_unitary_formula
TFFLFB_binding TFF_let_formula_binding

Instances

Eq TFF_let_formula_binding Source #
Methods (==) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool (/=) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool
Data TFF_let_formula_binding Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_let_formula_binding -> c TFF_let_formula_binding gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_let_formula_binding toConstr :: TFF_let_formula_binding -> Constr dataTypeOf :: TFF_let_formula_binding -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_let_formula_binding) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_let_formula_binding) gmapT :: (forall b. Data b => b -> b) -> TFF_let_formula_binding -> TFF_let_formula_binding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_binding -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_let_formula_binding -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_let_formula_binding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_let_formula_binding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_let_formula_binding -> m TFF_let_formula_binding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_binding -> m TFF_let_formula_binding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_let_formula_binding -> m TFF_let_formula_binding
Ord TFF_let_formula_binding Source #
Methods compare :: TFF_let_formula_binding -> TFF_let_formula_binding -> Ordering (<) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool (<=) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool (>) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool (>=) :: TFF_let_formula_binding -> TFF_let_formula_binding -> Bool max :: TFF_let_formula_binding -> TFF_let_formula_binding -> TFF_let_formula_binding min :: TFF_let_formula_binding -> TFF_let_formula_binding -> TFF_let_formula_binding
Show TFF_let_formula_binding Source #
Methods showsPrec :: Int -> TFF_let_formula_binding -> ShowS show :: TFF_let_formula_binding -> String showList :: [TFF_let_formula_binding] -> ShowS
GetRange TFF_let_formula_binding Source #
Methods getRange :: TFF_let_formula_binding -> Range Source # rangeSpan :: TFF_let_formula_binding -> [Pos] Source #

data TFF_sequent Source #

Constructors

TFFS_plain TFF_formula_tuple TFF_formula_tuple
TFFS_parens TFF_sequent

Instances

Eq TFF_sequent Source #
Methods (==) :: TFF_sequent -> TFF_sequent -> Bool (/=) :: TFF_sequent -> TFF_sequent -> Bool
Data TFF_sequent Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_sequent -> c TFF_sequent gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_sequent toConstr :: TFF_sequent -> Constr dataTypeOf :: TFF_sequent -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_sequent) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_sequent) gmapT :: (forall b. Data b => b -> b) -> TFF_sequent -> TFF_sequent gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_sequent -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_sequent -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_sequent -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_sequent -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_sequent -> m TFF_sequent gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_sequent -> m TFF_sequent gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_sequent -> m TFF_sequent
Ord TFF_sequent Source #
Methods compare :: TFF_sequent -> TFF_sequent -> Ordering (<) :: TFF_sequent -> TFF_sequent -> Bool (<=) :: TFF_sequent -> TFF_sequent -> Bool (>) :: TFF_sequent -> TFF_sequent -> Bool (>=) :: TFF_sequent -> TFF_sequent -> Bool max :: TFF_sequent -> TFF_sequent -> TFF_sequent min :: TFF_sequent -> TFF_sequent -> TFF_sequent
Show TFF_sequent Source #
Methods showsPrec :: Int -> TFF_sequent -> ShowS show :: TFF_sequent -> String showList :: [TFF_sequent] -> ShowS
GetRange TFF_sequent Source #
Methods getRange :: TFF_sequent -> Range Source # rangeSpan :: TFF_sequent -> [Pos] Source #

newtype TFF_formula_tuple Source #

Constructors

TFF_formula_tuple TFF_formula_tuple_list

Instances

Eq TFF_formula_tuple Source #
Methods (==) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool (/=) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool
Data TFF_formula_tuple Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_formula_tuple -> c TFF_formula_tuple gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_formula_tuple toConstr :: TFF_formula_tuple -> Constr dataTypeOf :: TFF_formula_tuple -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_formula_tuple) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_formula_tuple) gmapT :: (forall b. Data b => b -> b) -> TFF_formula_tuple -> TFF_formula_tuple gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_formula_tuple -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_formula_tuple -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_formula_tuple -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_formula_tuple -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_formula_tuple -> m TFF_formula_tuple gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_formula_tuple -> m TFF_formula_tuple gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_formula_tuple -> m TFF_formula_tuple
Ord TFF_formula_tuple Source #
Methods compare :: TFF_formula_tuple -> TFF_formula_tuple -> Ordering (<) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool (<=) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool (>) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool (>=) :: TFF_formula_tuple -> TFF_formula_tuple -> Bool max :: TFF_formula_tuple -> TFF_formula_tuple -> TFF_formula_tuple min :: TFF_formula_tuple -> TFF_formula_tuple -> TFF_formula_tuple
Show TFF_formula_tuple Source #
Methods showsPrec :: Int -> TFF_formula_tuple -> ShowS show :: TFF_formula_tuple -> String showList :: [TFF_formula_tuple] -> ShowS
GetRange TFF_formula_tuple Source #
Methods getRange :: TFF_formula_tuple -> Range Source # rangeSpan :: TFF_formula_tuple -> [Pos] Source #

type TFF_formula_tuple_list = [TFF_logic_formula] Source #

data TFF_typed_atom Source #

Constructors

TFFTA_plain Untyped_atom TFF_top_level_type
TFFTA_parens TFF_typed_atom

Instances

Eq TFF_typed_atom Source #
Methods (==) :: TFF_typed_atom -> TFF_typed_atom -> Bool (/=) :: TFF_typed_atom -> TFF_typed_atom -> Bool
Data TFF_typed_atom Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_typed_atom -> c TFF_typed_atom gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_typed_atom toConstr :: TFF_typed_atom -> Constr dataTypeOf :: TFF_typed_atom -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_typed_atom) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_typed_atom) gmapT :: (forall b. Data b => b -> b) -> TFF_typed_atom -> TFF_typed_atom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_typed_atom -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_typed_atom -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_typed_atom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_typed_atom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_typed_atom -> m TFF_typed_atom gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_typed_atom -> m TFF_typed_atom gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_typed_atom -> m TFF_typed_atom
Ord TFF_typed_atom Source #
Methods compare :: TFF_typed_atom -> TFF_typed_atom -> Ordering (<) :: TFF_typed_atom -> TFF_typed_atom -> Bool (<=) :: TFF_typed_atom -> TFF_typed_atom -> Bool (>) :: TFF_typed_atom -> TFF_typed_atom -> Bool (>=) :: TFF_typed_atom -> TFF_typed_atom -> Bool max :: TFF_typed_atom -> TFF_typed_atom -> TFF_typed_atom min :: TFF_typed_atom -> TFF_typed_atom -> TFF_typed_atom
Show TFF_typed_atom Source #
Methods showsPrec :: Int -> TFF_typed_atom -> ShowS show :: TFF_typed_atom -> String showList :: [TFF_typed_atom] -> ShowS
GetRange TFF_typed_atom Source #
Methods getRange :: TFF_typed_atom -> Range Source # rangeSpan :: TFF_typed_atom -> [Pos] Source #

data TFF_subtype Source #

Constructors

TFF_subtype Untyped_atom Atom

Instances

Eq TFF_subtype Source #
Methods (==) :: TFF_subtype -> TFF_subtype -> Bool (/=) :: TFF_subtype -> TFF_subtype -> Bool
Data TFF_subtype Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_subtype -> c TFF_subtype gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_subtype toConstr :: TFF_subtype -> Constr dataTypeOf :: TFF_subtype -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_subtype) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_subtype) gmapT :: (forall b. Data b => b -> b) -> TFF_subtype -> TFF_subtype gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_subtype -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_subtype -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_subtype -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_subtype -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_subtype -> m TFF_subtype gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_subtype -> m TFF_subtype gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_subtype -> m TFF_subtype
Ord TFF_subtype Source #
Methods compare :: TFF_subtype -> TFF_subtype -> Ordering (<) :: TFF_subtype -> TFF_subtype -> Bool (<=) :: TFF_subtype -> TFF_subtype -> Bool (>) :: TFF_subtype -> TFF_subtype -> Bool (>=) :: TFF_subtype -> TFF_subtype -> Bool max :: TFF_subtype -> TFF_subtype -> TFF_subtype min :: TFF_subtype -> TFF_subtype -> TFF_subtype
Show TFF_subtype Source #
Methods showsPrec :: Int -> TFF_subtype -> ShowS show :: TFF_subtype -> String showList :: [TFF_subtype] -> ShowS
GetRange TFF_subtype Source #
Methods getRange :: TFF_subtype -> Range Source # rangeSpan :: TFF_subtype -> [Pos] Source #

data TFF_top_level_type Source #

Constructors

TFFTLT_atomic TFF_atomic_type
TFFTLT_mapping TFF_mapping_type
TFFTLT_quantified TF1_quantified_type
TFFTLT_parens TFF_top_level_type

Instances

Eq TFF_top_level_type Source #
Methods (==) :: TFF_top_level_type -> TFF_top_level_type -> Bool (/=) :: TFF_top_level_type -> TFF_top_level_type -> Bool
Data TFF_top_level_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_top_level_type -> c TFF_top_level_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_top_level_type toConstr :: TFF_top_level_type -> Constr dataTypeOf :: TFF_top_level_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_top_level_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_top_level_type) gmapT :: (forall b. Data b => b -> b) -> TFF_top_level_type -> TFF_top_level_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_top_level_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_top_level_type -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_top_level_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_top_level_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_top_level_type -> m TFF_top_level_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_top_level_type -> m TFF_top_level_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_top_level_type -> m TFF_top_level_type
Ord TFF_top_level_type Source #
Methods compare :: TFF_top_level_type -> TFF_top_level_type -> Ordering (<) :: TFF_top_level_type -> TFF_top_level_type -> Bool (<=) :: TFF_top_level_type -> TFF_top_level_type -> Bool (>) :: TFF_top_level_type -> TFF_top_level_type -> Bool (>=) :: TFF_top_level_type -> TFF_top_level_type -> Bool max :: TFF_top_level_type -> TFF_top_level_type -> TFF_top_level_type min :: TFF_top_level_type -> TFF_top_level_type -> TFF_top_level_type
Show TFF_top_level_type Source #
Methods showsPrec :: Int -> TFF_top_level_type -> ShowS show :: TFF_top_level_type -> String showList :: [TFF_top_level_type] -> ShowS
GetRange TFF_top_level_type Source #
Methods getRange :: TFF_top_level_type -> Range Source # rangeSpan :: TFF_top_level_type -> [Pos] Source #

data TF1_quantified_type Source #

Constructors

TF1_quantified_type TFF_variable_list TFF_monotype

Instances

Eq TF1_quantified_type Source #
Methods (==) :: TF1_quantified_type -> TF1_quantified_type -> Bool (/=) :: TF1_quantified_type -> TF1_quantified_type -> Bool
Data TF1_quantified_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TF1_quantified_type -> c TF1_quantified_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TF1_quantified_type toConstr :: TF1_quantified_type -> Constr dataTypeOf :: TF1_quantified_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TF1_quantified_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TF1_quantified_type) gmapT :: (forall b. Data b => b -> b) -> TF1_quantified_type -> TF1_quantified_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TF1_quantified_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TF1_quantified_type -> r gmapQ :: (forall d. Data d => d -> u) -> TF1_quantified_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TF1_quantified_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TF1_quantified_type -> m TF1_quantified_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TF1_quantified_type -> m TF1_quantified_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TF1_quantified_type -> m TF1_quantified_type
Ord TF1_quantified_type Source #
Methods compare :: TF1_quantified_type -> TF1_quantified_type -> Ordering (<) :: TF1_quantified_type -> TF1_quantified_type -> Bool (<=) :: TF1_quantified_type -> TF1_quantified_type -> Bool (>) :: TF1_quantified_type -> TF1_quantified_type -> Bool (>=) :: TF1_quantified_type -> TF1_quantified_type -> Bool max :: TF1_quantified_type -> TF1_quantified_type -> TF1_quantified_type min :: TF1_quantified_type -> TF1_quantified_type -> TF1_quantified_type
Show TF1_quantified_type Source #
Methods showsPrec :: Int -> TF1_quantified_type -> ShowS show :: TF1_quantified_type -> String showList :: [TF1_quantified_type] -> ShowS
GetRange TF1_quantified_type Source #
Methods getRange :: TF1_quantified_type -> Range Source # rangeSpan :: TF1_quantified_type -> [Pos] Source #

data TFF_monotype Source #

Constructors

TFFMT_atomic TFF_atomic_type
TFFMT_mapping TFF_mapping_type

Instances

Eq TFF_monotype Source #
Methods (==) :: TFF_monotype -> TFF_monotype -> Bool (/=) :: TFF_monotype -> TFF_monotype -> Bool
Data TFF_monotype Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_monotype -> c TFF_monotype gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_monotype toConstr :: TFF_monotype -> Constr dataTypeOf :: TFF_monotype -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_monotype) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_monotype) gmapT :: (forall b. Data b => b -> b) -> TFF_monotype -> TFF_monotype gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_monotype -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_monotype -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_monotype -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_monotype -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_monotype -> m TFF_monotype gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_monotype -> m TFF_monotype gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_monotype -> m TFF_monotype
Ord TFF_monotype Source #
Methods compare :: TFF_monotype -> TFF_monotype -> Ordering (<) :: TFF_monotype -> TFF_monotype -> Bool (<=) :: TFF_monotype -> TFF_monotype -> Bool (>) :: TFF_monotype -> TFF_monotype -> Bool (>=) :: TFF_monotype -> TFF_monotype -> Bool max :: TFF_monotype -> TFF_monotype -> TFF_monotype min :: TFF_monotype -> TFF_monotype -> TFF_monotype
Show TFF_monotype Source #
Methods showsPrec :: Int -> TFF_monotype -> ShowS show :: TFF_monotype -> String showList :: [TFF_monotype] -> ShowS
GetRange TFF_monotype Source #
Methods getRange :: TFF_monotype -> Range Source # rangeSpan :: TFF_monotype -> [Pos] Source #

data TFF_unitary_type Source #

Constructors

TFFUT_atomic TFF_atomic_type
TFFUT_xprod TFF_xprod_type

Instances

Eq TFF_unitary_type Source #
Methods (==) :: TFF_unitary_type -> TFF_unitary_type -> Bool (/=) :: TFF_unitary_type -> TFF_unitary_type -> Bool
Data TFF_unitary_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_unitary_type -> c TFF_unitary_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_unitary_type toConstr :: TFF_unitary_type -> Constr dataTypeOf :: TFF_unitary_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_unitary_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_unitary_type) gmapT :: (forall b. Data b => b -> b) -> TFF_unitary_type -> TFF_unitary_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unitary_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_unitary_type -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_unitary_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_unitary_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_unitary_type -> m TFF_unitary_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unitary_type -> m TFF_unitary_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_unitary_type -> m TFF_unitary_type
Ord TFF_unitary_type Source #
Methods compare :: TFF_unitary_type -> TFF_unitary_type -> Ordering (<) :: TFF_unitary_type -> TFF_unitary_type -> Bool (<=) :: TFF_unitary_type -> TFF_unitary_type -> Bool (>) :: TFF_unitary_type -> TFF_unitary_type -> Bool (>=) :: TFF_unitary_type -> TFF_unitary_type -> Bool max :: TFF_unitary_type -> TFF_unitary_type -> TFF_unitary_type min :: TFF_unitary_type -> TFF_unitary_type -> TFF_unitary_type
Show TFF_unitary_type Source #
Methods showsPrec :: Int -> TFF_unitary_type -> ShowS show :: TFF_unitary_type -> String showList :: [TFF_unitary_type] -> ShowS
GetRange TFF_unitary_type Source #
Methods getRange :: TFF_unitary_type -> Range Source # rangeSpan :: TFF_unitary_type -> [Pos] Source #

data TFF_atomic_type Source #

Constructors

TFFAT_constant Type_constant
TFFAT_defined Defined_type
TFFAT_functor Type_functor TFF_type_arguments
TFFAT_variable Variable

Instances

Eq TFF_atomic_type Source #
Methods (==) :: TFF_atomic_type -> TFF_atomic_type -> Bool (/=) :: TFF_atomic_type -> TFF_atomic_type -> Bool
Data TFF_atomic_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_atomic_type -> c TFF_atomic_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_atomic_type toConstr :: TFF_atomic_type -> Constr dataTypeOf :: TFF_atomic_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_atomic_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_atomic_type) gmapT :: (forall b. Data b => b -> b) -> TFF_atomic_type -> TFF_atomic_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_atomic_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_atomic_type -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_atomic_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_atomic_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_atomic_type -> m TFF_atomic_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_atomic_type -> m TFF_atomic_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_atomic_type -> m TFF_atomic_type
Ord TFF_atomic_type Source #
Methods compare :: TFF_atomic_type -> TFF_atomic_type -> Ordering (<) :: TFF_atomic_type -> TFF_atomic_type -> Bool (<=) :: TFF_atomic_type -> TFF_atomic_type -> Bool (>) :: TFF_atomic_type -> TFF_atomic_type -> Bool (>=) :: TFF_atomic_type -> TFF_atomic_type -> Bool max :: TFF_atomic_type -> TFF_atomic_type -> TFF_atomic_type min :: TFF_atomic_type -> TFF_atomic_type -> TFF_atomic_type
Show TFF_atomic_type Source #
Methods showsPrec :: Int -> TFF_atomic_type -> ShowS show :: TFF_atomic_type -> String showList :: [TFF_atomic_type] -> ShowS
GetRange TFF_atomic_type Source #
Methods getRange :: TFF_atomic_type -> Range Source # rangeSpan :: TFF_atomic_type -> [Pos] Source #

type TFF_type_arguments = [TFF_atomic_type] Source #

data TFF_mapping_type Source #

Constructors

TFF_mapping_type TFF_unitary_type TFF_atomic_type

Instances

Eq TFF_mapping_type Source #
Methods (==) :: TFF_mapping_type -> TFF_mapping_type -> Bool (/=) :: TFF_mapping_type -> TFF_mapping_type -> Bool
Data TFF_mapping_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_mapping_type -> c TFF_mapping_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_mapping_type toConstr :: TFF_mapping_type -> Constr dataTypeOf :: TFF_mapping_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_mapping_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_mapping_type) gmapT :: (forall b. Data b => b -> b) -> TFF_mapping_type -> TFF_mapping_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_mapping_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_mapping_type -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_mapping_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_mapping_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_mapping_type -> m TFF_mapping_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_mapping_type -> m TFF_mapping_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_mapping_type -> m TFF_mapping_type
Ord TFF_mapping_type Source #
Methods compare :: TFF_mapping_type -> TFF_mapping_type -> Ordering (<) :: TFF_mapping_type -> TFF_mapping_type -> Bool (<=) :: TFF_mapping_type -> TFF_mapping_type -> Bool (>) :: TFF_mapping_type -> TFF_mapping_type -> Bool (>=) :: TFF_mapping_type -> TFF_mapping_type -> Bool max :: TFF_mapping_type -> TFF_mapping_type -> TFF_mapping_type min :: TFF_mapping_type -> TFF_mapping_type -> TFF_mapping_type
Show TFF_mapping_type Source #
Methods showsPrec :: Int -> TFF_mapping_type -> ShowS show :: TFF_mapping_type -> String showList :: [TFF_mapping_type] -> ShowS
GetRange TFF_mapping_type Source #
Methods getRange :: TFF_mapping_type -> Range Source # rangeSpan :: TFF_mapping_type -> [Pos] Source #

data TFF_xprod_type Source #

Constructors

TFF_xprod_type TFF_unitary_type [TFF_atomic_type]

Instances

Eq TFF_xprod_type Source #
Methods (==) :: TFF_xprod_type -> TFF_xprod_type -> Bool (/=) :: TFF_xprod_type -> TFF_xprod_type -> Bool
Data TFF_xprod_type Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TFF_xprod_type -> c TFF_xprod_type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TFF_xprod_type toConstr :: TFF_xprod_type -> Constr dataTypeOf :: TFF_xprod_type -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TFF_xprod_type) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TFF_xprod_type) gmapT :: (forall b. Data b => b -> b) -> TFF_xprod_type -> TFF_xprod_type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TFF_xprod_type -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TFF_xprod_type -> r gmapQ :: (forall d. Data d => d -> u) -> TFF_xprod_type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TFF_xprod_type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TFF_xprod_type -> m TFF_xprod_type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_xprod_type -> m TFF_xprod_type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TFF_xprod_type -> m TFF_xprod_type
Ord TFF_xprod_type Source #
Methods compare :: TFF_xprod_type -> TFF_xprod_type -> Ordering (<) :: TFF_xprod_type -> TFF_xprod_type -> Bool (<=) :: TFF_xprod_type -> TFF_xprod_type -> Bool (>) :: TFF_xprod_type -> TFF_xprod_type -> Bool (>=) :: TFF_xprod_type -> TFF_xprod_type -> Bool max :: TFF_xprod_type -> TFF_xprod_type -> TFF_xprod_type min :: TFF_xprod_type -> TFF_xprod_type -> TFF_xprod_type
Show TFF_xprod_type Source #
Methods showsPrec :: Int -> TFF_xprod_type -> ShowS show :: TFF_xprod_type -> String showList :: [TFF_xprod_type] -> ShowS
GetRange TFF_xprod_type Source #
Methods getRange :: TFF_xprod_type -> Range Source # rangeSpan :: TFF_xprod_type -> [Pos] Source #

data TCF_formula Source #

Constructors

TCFF_logic TCF_logic_formula
TCFF_atom TFF_typed_atom

Instances

Eq TCF_formula Source #
Methods (==) :: TCF_formula -> TCF_formula -> Bool (/=) :: TCF_formula -> TCF_formula -> Bool
Data TCF_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCF_formula -> c TCF_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCF_formula toConstr :: TCF_formula -> Constr dataTypeOf :: TCF_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TCF_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCF_formula) gmapT :: (forall b. Data b => b -> b) -> TCF_formula -> TCF_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCF_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCF_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TCF_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TCF_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCF_formula -> m TCF_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_formula -> m TCF_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_formula -> m TCF_formula
Ord TCF_formula Source #
Methods compare :: TCF_formula -> TCF_formula -> Ordering (<) :: TCF_formula -> TCF_formula -> Bool (<=) :: TCF_formula -> TCF_formula -> Bool (>) :: TCF_formula -> TCF_formula -> Bool (>=) :: TCF_formula -> TCF_formula -> Bool max :: TCF_formula -> TCF_formula -> TCF_formula min :: TCF_formula -> TCF_formula -> TCF_formula
Show TCF_formula Source #
Methods showsPrec :: Int -> TCF_formula -> ShowS show :: TCF_formula -> String showList :: [TCF_formula] -> ShowS
GetRange TCF_formula Source #
Methods getRange :: TCF_formula -> Range Source # rangeSpan :: TCF_formula -> [Pos] Source #

data TCF_logic_formula Source #

Constructors

TCFLF_quantified TCF_quantified_formula
TCFLF_cnf CNF_formula

Instances

Eq TCF_logic_formula Source #
Methods (==) :: TCF_logic_formula -> TCF_logic_formula -> Bool (/=) :: TCF_logic_formula -> TCF_logic_formula -> Bool
Data TCF_logic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCF_logic_formula -> c TCF_logic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCF_logic_formula toConstr :: TCF_logic_formula -> Constr dataTypeOf :: TCF_logic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TCF_logic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCF_logic_formula) gmapT :: (forall b. Data b => b -> b) -> TCF_logic_formula -> TCF_logic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCF_logic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCF_logic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TCF_logic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TCF_logic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCF_logic_formula -> m TCF_logic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_logic_formula -> m TCF_logic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_logic_formula -> m TCF_logic_formula
Ord TCF_logic_formula Source #
Methods compare :: TCF_logic_formula -> TCF_logic_formula -> Ordering (<) :: TCF_logic_formula -> TCF_logic_formula -> Bool (<=) :: TCF_logic_formula -> TCF_logic_formula -> Bool (>) :: TCF_logic_formula -> TCF_logic_formula -> Bool (>=) :: TCF_logic_formula -> TCF_logic_formula -> Bool max :: TCF_logic_formula -> TCF_logic_formula -> TCF_logic_formula min :: TCF_logic_formula -> TCF_logic_formula -> TCF_logic_formula
Show TCF_logic_formula Source #
Methods showsPrec :: Int -> TCF_logic_formula -> ShowS show :: TCF_logic_formula -> String showList :: [TCF_logic_formula] -> ShowS
GetRange TCF_logic_formula Source #
Methods getRange :: TCF_logic_formula -> Range Source # rangeSpan :: TCF_logic_formula -> [Pos] Source #

data TCF_quantified_formula Source #

Constructors

TCF_quantified TFF_variable_list CNF_formula

Instances

Eq TCF_quantified_formula Source #
Methods (==) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool (/=) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool
Data TCF_quantified_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCF_quantified_formula -> c TCF_quantified_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCF_quantified_formula toConstr :: TCF_quantified_formula -> Constr dataTypeOf :: TCF_quantified_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TCF_quantified_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCF_quantified_formula) gmapT :: (forall b. Data b => b -> b) -> TCF_quantified_formula -> TCF_quantified_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCF_quantified_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCF_quantified_formula -> r gmapQ :: (forall d. Data d => d -> u) -> TCF_quantified_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TCF_quantified_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCF_quantified_formula -> m TCF_quantified_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_quantified_formula -> m TCF_quantified_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCF_quantified_formula -> m TCF_quantified_formula
Ord TCF_quantified_formula Source #
Methods compare :: TCF_quantified_formula -> TCF_quantified_formula -> Ordering (<) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool (<=) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool (>) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool (>=) :: TCF_quantified_formula -> TCF_quantified_formula -> Bool max :: TCF_quantified_formula -> TCF_quantified_formula -> TCF_quantified_formula min :: TCF_quantified_formula -> TCF_quantified_formula -> TCF_quantified_formula
Show TCF_quantified_formula Source #
Methods showsPrec :: Int -> TCF_quantified_formula -> ShowS show :: TCF_quantified_formula -> String showList :: [TCF_quantified_formula] -> ShowS
GetRange TCF_quantified_formula Source #
Methods getRange :: TCF_quantified_formula -> Range Source # rangeSpan :: TCF_quantified_formula -> [Pos] Source #

data FOF_formula Source #

Constructors

FOFF_logic FOF_logic_formula
FOFF_sequent FOF_sequent

Instances

Eq FOF_formula Source #
Methods (==) :: FOF_formula -> FOF_formula -> Bool (/=) :: FOF_formula -> FOF_formula -> Bool
Data FOF_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_formula -> c FOF_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_formula toConstr :: FOF_formula -> Constr dataTypeOf :: FOF_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_formula -> FOF_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_formula -> m FOF_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_formula -> m FOF_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_formula -> m FOF_formula
Ord FOF_formula Source #
Methods compare :: FOF_formula -> FOF_formula -> Ordering (<) :: FOF_formula -> FOF_formula -> Bool (<=) :: FOF_formula -> FOF_formula -> Bool (>) :: FOF_formula -> FOF_formula -> Bool (>=) :: FOF_formula -> FOF_formula -> Bool max :: FOF_formula -> FOF_formula -> FOF_formula min :: FOF_formula -> FOF_formula -> FOF_formula
Show FOF_formula Source #
Methods showsPrec :: Int -> FOF_formula -> ShowS show :: FOF_formula -> String showList :: [FOF_formula] -> ShowS
GetRange FOF_formula Source #
Methods getRange :: FOF_formula -> Range Source # rangeSpan :: FOF_formula -> [Pos] Source #

data FOF_logic_formula Source #

Constructors

FOFLF_binary FOF_binary_formula
FOFLF_unitary FOF_unitary_formula

Instances

Eq FOF_logic_formula Source #
Methods (==) :: FOF_logic_formula -> FOF_logic_formula -> Bool (/=) :: FOF_logic_formula -> FOF_logic_formula -> Bool
Data FOF_logic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_logic_formula -> c FOF_logic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_logic_formula toConstr :: FOF_logic_formula -> Constr dataTypeOf :: FOF_logic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_logic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_logic_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_logic_formula -> FOF_logic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_logic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_logic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_logic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_logic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_logic_formula -> m FOF_logic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_logic_formula -> m FOF_logic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_logic_formula -> m FOF_logic_formula
Ord FOF_logic_formula Source #
Methods compare :: FOF_logic_formula -> FOF_logic_formula -> Ordering (<) :: FOF_logic_formula -> FOF_logic_formula -> Bool (<=) :: FOF_logic_formula -> FOF_logic_formula -> Bool (>) :: FOF_logic_formula -> FOF_logic_formula -> Bool (>=) :: FOF_logic_formula -> FOF_logic_formula -> Bool max :: FOF_logic_formula -> FOF_logic_formula -> FOF_logic_formula min :: FOF_logic_formula -> FOF_logic_formula -> FOF_logic_formula
Show FOF_logic_formula Source #
Methods showsPrec :: Int -> FOF_logic_formula -> ShowS show :: FOF_logic_formula -> String showList :: [FOF_logic_formula] -> ShowS
GetRange FOF_logic_formula Source #
Methods getRange :: FOF_logic_formula -> Range Source # rangeSpan :: FOF_logic_formula -> [Pos] Source #

data FOF_binary_formula Source #

Constructors

FOFBF_nonassoc FOF_binary_nonassoc
FOFBF_assoc FOF_binary_assoc

Instances

Eq FOF_binary_formula Source #
Methods (==) :: FOF_binary_formula -> FOF_binary_formula -> Bool (/=) :: FOF_binary_formula -> FOF_binary_formula -> Bool
Data FOF_binary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_binary_formula -> c FOF_binary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_binary_formula toConstr :: FOF_binary_formula -> Constr dataTypeOf :: FOF_binary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_binary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_binary_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_binary_formula -> FOF_binary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_binary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_binary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_binary_formula -> m FOF_binary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_formula -> m FOF_binary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_formula -> m FOF_binary_formula
Ord FOF_binary_formula Source #
Methods compare :: FOF_binary_formula -> FOF_binary_formula -> Ordering (<) :: FOF_binary_formula -> FOF_binary_formula -> Bool (<=) :: FOF_binary_formula -> FOF_binary_formula -> Bool (>) :: FOF_binary_formula -> FOF_binary_formula -> Bool (>=) :: FOF_binary_formula -> FOF_binary_formula -> Bool max :: FOF_binary_formula -> FOF_binary_formula -> FOF_binary_formula min :: FOF_binary_formula -> FOF_binary_formula -> FOF_binary_formula
Show FOF_binary_formula Source #
Methods showsPrec :: Int -> FOF_binary_formula -> ShowS show :: FOF_binary_formula -> String showList :: [FOF_binary_formula] -> ShowS
GetRange FOF_binary_formula Source #
Methods getRange :: FOF_binary_formula -> Range Source # rangeSpan :: FOF_binary_formula -> [Pos] Source #

data FOF_binary_nonassoc Source #

Constructors

FOF_binary_nonassoc Binary_connective FOF_unitary_formula FOF_unitary_formula

Instances

Eq FOF_binary_nonassoc Source #
Methods (==) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool (/=) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool
Data FOF_binary_nonassoc Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_binary_nonassoc -> c FOF_binary_nonassoc gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_binary_nonassoc toConstr :: FOF_binary_nonassoc -> Constr dataTypeOf :: FOF_binary_nonassoc -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_binary_nonassoc) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_binary_nonassoc) gmapT :: (forall b. Data b => b -> b) -> FOF_binary_nonassoc -> FOF_binary_nonassoc gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_nonassoc -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_nonassoc -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_binary_nonassoc -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_binary_nonassoc -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_binary_nonassoc -> m FOF_binary_nonassoc gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_nonassoc -> m FOF_binary_nonassoc gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_nonassoc -> m FOF_binary_nonassoc
Ord FOF_binary_nonassoc Source #
Methods compare :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Ordering (<) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool (<=) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool (>) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool (>=) :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> Bool max :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> FOF_binary_nonassoc min :: FOF_binary_nonassoc -> FOF_binary_nonassoc -> FOF_binary_nonassoc
Show FOF_binary_nonassoc Source #
Methods showsPrec :: Int -> FOF_binary_nonassoc -> ShowS show :: FOF_binary_nonassoc -> String showList :: [FOF_binary_nonassoc] -> ShowS
GetRange FOF_binary_nonassoc Source #
Methods getRange :: FOF_binary_nonassoc -> Range Source # rangeSpan :: FOF_binary_nonassoc -> [Pos] Source #

data FOF_binary_assoc Source #

Constructors

FOFBA_or FOF_or_formula
FOFBA_and FOF_and_formula

Instances

Eq FOF_binary_assoc Source #
Methods (==) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool (/=) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool
Data FOF_binary_assoc Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_binary_assoc -> c FOF_binary_assoc gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_binary_assoc toConstr :: FOF_binary_assoc -> Constr dataTypeOf :: FOF_binary_assoc -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_binary_assoc) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_binary_assoc) gmapT :: (forall b. Data b => b -> b) -> FOF_binary_assoc -> FOF_binary_assoc gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_assoc -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_binary_assoc -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_binary_assoc -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_binary_assoc -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_binary_assoc -> m FOF_binary_assoc gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_assoc -> m FOF_binary_assoc gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_binary_assoc -> m FOF_binary_assoc
Ord FOF_binary_assoc Source #
Methods compare :: FOF_binary_assoc -> FOF_binary_assoc -> Ordering (<) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool (<=) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool (>) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool (>=) :: FOF_binary_assoc -> FOF_binary_assoc -> Bool max :: FOF_binary_assoc -> FOF_binary_assoc -> FOF_binary_assoc min :: FOF_binary_assoc -> FOF_binary_assoc -> FOF_binary_assoc
Show FOF_binary_assoc Source #
Methods showsPrec :: Int -> FOF_binary_assoc -> ShowS show :: FOF_binary_assoc -> String showList :: [FOF_binary_assoc] -> ShowS
GetRange FOF_binary_assoc Source #
Methods getRange :: FOF_binary_assoc -> Range Source # rangeSpan :: FOF_binary_assoc -> [Pos] Source #

type FOF_or_formula = [FOF_unitary_formula] Source #

type FOF_and_formula = [FOF_unitary_formula] Source #

data FOF_unitary_formula Source #

Constructors

FOFUF_quantified FOF_quantified_formula
FOFUF_unary FOF_unary_formula
FOFUF_atomic FOF_atomic_formula
FOFUF_logic FOF_logic_formula

Instances

Eq FOF_unitary_formula Source #
Methods (==) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool (/=) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool
Data FOF_unitary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_unitary_formula -> c FOF_unitary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_unitary_formula toConstr :: FOF_unitary_formula -> Constr dataTypeOf :: FOF_unitary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_unitary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_unitary_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_unitary_formula -> FOF_unitary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_unitary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_unitary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_unitary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_unitary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_unitary_formula -> m FOF_unitary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_unitary_formula -> m FOF_unitary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_unitary_formula -> m FOF_unitary_formula
Ord FOF_unitary_formula Source #
Methods compare :: FOF_unitary_formula -> FOF_unitary_formula -> Ordering (<) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool (<=) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool (>) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool (>=) :: FOF_unitary_formula -> FOF_unitary_formula -> Bool max :: FOF_unitary_formula -> FOF_unitary_formula -> FOF_unitary_formula min :: FOF_unitary_formula -> FOF_unitary_formula -> FOF_unitary_formula
Show FOF_unitary_formula Source #
Methods showsPrec :: Int -> FOF_unitary_formula -> ShowS show :: FOF_unitary_formula -> String showList :: [FOF_unitary_formula] -> ShowS
GetRange FOF_unitary_formula Source #
Methods getRange :: FOF_unitary_formula -> Range Source # rangeSpan :: FOF_unitary_formula -> [Pos] Source #

data FOF_quantified_formula Source #

Constructors

FOF_quantified_formula FOF_quantifier FOF_variable_list FOF_unitary_formula

Instances

Eq FOF_quantified_formula Source #
Methods (==) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool (/=) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool
Data FOF_quantified_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_quantified_formula -> c FOF_quantified_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_quantified_formula toConstr :: FOF_quantified_formula -> Constr dataTypeOf :: FOF_quantified_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_quantified_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_quantified_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_quantified_formula -> FOF_quantified_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_quantified_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_quantified_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_quantified_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_quantified_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_quantified_formula -> m FOF_quantified_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_quantified_formula -> m FOF_quantified_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_quantified_formula -> m FOF_quantified_formula
Ord FOF_quantified_formula Source #
Methods compare :: FOF_quantified_formula -> FOF_quantified_formula -> Ordering (<) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool (<=) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool (>) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool (>=) :: FOF_quantified_formula -> FOF_quantified_formula -> Bool max :: FOF_quantified_formula -> FOF_quantified_formula -> FOF_quantified_formula min :: FOF_quantified_formula -> FOF_quantified_formula -> FOF_quantified_formula
Show FOF_quantified_formula Source #
Methods showsPrec :: Int -> FOF_quantified_formula -> ShowS show :: FOF_quantified_formula -> String showList :: [FOF_quantified_formula] -> ShowS
GetRange FOF_quantified_formula Source #
Methods getRange :: FOF_quantified_formula -> Range Source # rangeSpan :: FOF_quantified_formula -> [Pos] Source #

type FOF_variable_list = [Variable] Source #

data FOF_unary_formula Source #

Constructors

FOFUF_connective Unary_connective FOF_unitary_formula
FOFUF_infix FOF_infix_unary

Instances

Eq FOF_unary_formula Source #
Methods (==) :: FOF_unary_formula -> FOF_unary_formula -> Bool (/=) :: FOF_unary_formula -> FOF_unary_formula -> Bool
Data FOF_unary_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_unary_formula -> c FOF_unary_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_unary_formula toConstr :: FOF_unary_formula -> Constr dataTypeOf :: FOF_unary_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_unary_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_unary_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_unary_formula -> FOF_unary_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_unary_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_unary_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_unary_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_unary_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_unary_formula -> m FOF_unary_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_unary_formula -> m FOF_unary_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_unary_formula -> m FOF_unary_formula
Ord FOF_unary_formula Source #
Methods compare :: FOF_unary_formula -> FOF_unary_formula -> Ordering (<) :: FOF_unary_formula -> FOF_unary_formula -> Bool (<=) :: FOF_unary_formula -> FOF_unary_formula -> Bool (>) :: FOF_unary_formula -> FOF_unary_formula -> Bool (>=) :: FOF_unary_formula -> FOF_unary_formula -> Bool max :: FOF_unary_formula -> FOF_unary_formula -> FOF_unary_formula min :: FOF_unary_formula -> FOF_unary_formula -> FOF_unary_formula
Show FOF_unary_formula Source #
Methods showsPrec :: Int -> FOF_unary_formula -> ShowS show :: FOF_unary_formula -> String showList :: [FOF_unary_formula] -> ShowS
GetRange FOF_unary_formula Source #
Methods getRange :: FOF_unary_formula -> Range Source # rangeSpan :: FOF_unary_formula -> [Pos] Source #

data FOF_infix_unary Source #

Constructors

FOF_infix_unary FOF_term FOF_term

Instances

Eq FOF_infix_unary Source #
Methods (==) :: FOF_infix_unary -> FOF_infix_unary -> Bool (/=) :: FOF_infix_unary -> FOF_infix_unary -> Bool
Data FOF_infix_unary Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_infix_unary -> c FOF_infix_unary gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_infix_unary toConstr :: FOF_infix_unary -> Constr dataTypeOf :: FOF_infix_unary -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_infix_unary) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_infix_unary) gmapT :: (forall b. Data b => b -> b) -> FOF_infix_unary -> FOF_infix_unary gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_infix_unary -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_infix_unary -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_infix_unary -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_infix_unary -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_infix_unary -> m FOF_infix_unary gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_infix_unary -> m FOF_infix_unary gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_infix_unary -> m FOF_infix_unary
Ord FOF_infix_unary Source #
Methods compare :: FOF_infix_unary -> FOF_infix_unary -> Ordering (<) :: FOF_infix_unary -> FOF_infix_unary -> Bool (<=) :: FOF_infix_unary -> FOF_infix_unary -> Bool (>) :: FOF_infix_unary -> FOF_infix_unary -> Bool (>=) :: FOF_infix_unary -> FOF_infix_unary -> Bool max :: FOF_infix_unary -> FOF_infix_unary -> FOF_infix_unary min :: FOF_infix_unary -> FOF_infix_unary -> FOF_infix_unary
Show FOF_infix_unary Source #
Methods showsPrec :: Int -> FOF_infix_unary -> ShowS show :: FOF_infix_unary -> String showList :: [FOF_infix_unary] -> ShowS
GetRange FOF_infix_unary Source #
Methods getRange :: FOF_infix_unary -> Range Source # rangeSpan :: FOF_infix_unary -> [Pos] Source #

data FOF_atomic_formula Source #

Constructors

FOFAT_plain FOF_plain_atomic_formula
FOFAT_defined FOF_defined_atomic_formula
FOFAT_system FOF_system_atomic_formula

Instances

Eq FOF_atomic_formula Source #
Methods (==) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool (/=) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool
Data FOF_atomic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_atomic_formula -> c FOF_atomic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_atomic_formula toConstr :: FOF_atomic_formula -> Constr dataTypeOf :: FOF_atomic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_atomic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_atomic_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_atomic_formula -> FOF_atomic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_atomic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_atomic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_atomic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_atomic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_atomic_formula -> m FOF_atomic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_atomic_formula -> m FOF_atomic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_atomic_formula -> m FOF_atomic_formula
Ord FOF_atomic_formula Source #
Methods compare :: FOF_atomic_formula -> FOF_atomic_formula -> Ordering (<) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool (<=) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool (>) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool (>=) :: FOF_atomic_formula -> FOF_atomic_formula -> Bool max :: FOF_atomic_formula -> FOF_atomic_formula -> FOF_atomic_formula min :: FOF_atomic_formula -> FOF_atomic_formula -> FOF_atomic_formula
Show FOF_atomic_formula Source #
Methods showsPrec :: Int -> FOF_atomic_formula -> ShowS show :: FOF_atomic_formula -> String showList :: [FOF_atomic_formula] -> ShowS
GetRange FOF_atomic_formula Source #
Methods getRange :: FOF_atomic_formula -> Range Source # rangeSpan :: FOF_atomic_formula -> [Pos] Source #

data FOF_plain_atomic_formula Source #

Constructors

FOFPAF_proposition Proposition
FOFPAF_predicate Predicate FOF_arguments

Instances

Eq FOF_plain_atomic_formula Source #
Methods (==) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool (/=) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool
Data FOF_plain_atomic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_plain_atomic_formula -> c FOF_plain_atomic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_plain_atomic_formula toConstr :: FOF_plain_atomic_formula -> Constr dataTypeOf :: FOF_plain_atomic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_plain_atomic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_plain_atomic_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_plain_atomic_formula -> FOF_plain_atomic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_plain_atomic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_plain_atomic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_plain_atomic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_plain_atomic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_plain_atomic_formula -> m FOF_plain_atomic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_plain_atomic_formula -> m FOF_plain_atomic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_plain_atomic_formula -> m FOF_plain_atomic_formula
Ord FOF_plain_atomic_formula Source #
Methods compare :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Ordering (<) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool (<=) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool (>) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool (>=) :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> Bool max :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> FOF_plain_atomic_formula min :: FOF_plain_atomic_formula -> FOF_plain_atomic_formula -> FOF_plain_atomic_formula
Show FOF_plain_atomic_formula Source #
Methods showsPrec :: Int -> FOF_plain_atomic_formula -> ShowS show :: FOF_plain_atomic_formula -> String showList :: [FOF_plain_atomic_formula] -> ShowS
GetRange FOF_plain_atomic_formula Source #
Methods getRange :: FOF_plain_atomic_formula -> Range Source # rangeSpan :: FOF_plain_atomic_formula -> [Pos] Source #

data FOF_defined_atomic_formula Source #

Constructors

FOFDAF_plain FOF_defined_plain_formula
FOFDAF_infix FOF_defined_infix_formula

Instances

Eq FOF_defined_atomic_formula Source #
Methods (==) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool (/=) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool
Data FOF_defined_atomic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_defined_atomic_formula -> c FOF_defined_atomic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_defined_atomic_formula toConstr :: FOF_defined_atomic_formula -> Constr dataTypeOf :: FOF_defined_atomic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_defined_atomic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_defined_atomic_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_defined_atomic_formula -> FOF_defined_atomic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_atomic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_atomic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_defined_atomic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_defined_atomic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_defined_atomic_formula -> m FOF_defined_atomic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_atomic_formula -> m FOF_defined_atomic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_atomic_formula -> m FOF_defined_atomic_formula
Ord FOF_defined_atomic_formula Source #
Methods compare :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Ordering (<) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool (<=) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool (>) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool (>=) :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> Bool max :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> FOF_defined_atomic_formula min :: FOF_defined_atomic_formula -> FOF_defined_atomic_formula -> FOF_defined_atomic_formula
Show FOF_defined_atomic_formula Source #
Methods showsPrec :: Int -> FOF_defined_atomic_formula -> ShowS show :: FOF_defined_atomic_formula -> String showList :: [FOF_defined_atomic_formula] -> ShowS
GetRange FOF_defined_atomic_formula Source #
Methods getRange :: FOF_defined_atomic_formula -> Range Source # rangeSpan :: FOF_defined_atomic_formula -> [Pos] Source #

data FOF_defined_plain_formula Source #

Constructors

FOFDPF_proposition Defined_proposition
FOFDPF_predicate Defined_predicate FOF_arguments

Instances

Eq FOF_defined_plain_formula Source #
Methods (==) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool (/=) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool
Data FOF_defined_plain_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_defined_plain_formula -> c FOF_defined_plain_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_defined_plain_formula toConstr :: FOF_defined_plain_formula -> Constr dataTypeOf :: FOF_defined_plain_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_defined_plain_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_defined_plain_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_defined_plain_formula -> FOF_defined_plain_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_plain_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_plain_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_defined_plain_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_defined_plain_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_defined_plain_formula -> m FOF_defined_plain_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_plain_formula -> m FOF_defined_plain_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_plain_formula -> m FOF_defined_plain_formula
Ord FOF_defined_plain_formula Source #
Methods compare :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Ordering (<) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool (<=) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool (>) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool (>=) :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> Bool max :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> FOF_defined_plain_formula min :: FOF_defined_plain_formula -> FOF_defined_plain_formula -> FOF_defined_plain_formula
Show FOF_defined_plain_formula Source #
Methods showsPrec :: Int -> FOF_defined_plain_formula -> ShowS show :: FOF_defined_plain_formula -> String showList :: [FOF_defined_plain_formula] -> ShowS
GetRange FOF_defined_plain_formula Source #
Methods getRange :: FOF_defined_plain_formula -> Range Source # rangeSpan :: FOF_defined_plain_formula -> [Pos] Source #

data FOF_defined_infix_formula Source #

Constructors

FOF_defined_infix_formula Defined_infix_pred FOF_term FOF_term

Instances

Eq FOF_defined_infix_formula Source #
Methods (==) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool (/=) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool
Data FOF_defined_infix_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_defined_infix_formula -> c FOF_defined_infix_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_defined_infix_formula toConstr :: FOF_defined_infix_formula -> Constr dataTypeOf :: FOF_defined_infix_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_defined_infix_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_defined_infix_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_defined_infix_formula -> FOF_defined_infix_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_infix_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_infix_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_defined_infix_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_defined_infix_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_defined_infix_formula -> m FOF_defined_infix_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_infix_formula -> m FOF_defined_infix_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_infix_formula -> m FOF_defined_infix_formula
Ord FOF_defined_infix_formula Source #
Methods compare :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Ordering (<) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool (<=) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool (>) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool (>=) :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> Bool max :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> FOF_defined_infix_formula min :: FOF_defined_infix_formula -> FOF_defined_infix_formula -> FOF_defined_infix_formula
Show FOF_defined_infix_formula Source #
Methods showsPrec :: Int -> FOF_defined_infix_formula -> ShowS show :: FOF_defined_infix_formula -> String showList :: [FOF_defined_infix_formula] -> ShowS
GetRange FOF_defined_infix_formula Source #
Methods getRange :: FOF_defined_infix_formula -> Range Source # rangeSpan :: FOF_defined_infix_formula -> [Pos] Source #

newtype FOF_system_atomic_formula Source #

Constructors

FOF_system_atomic_formula FOF_system_term

Instances

Eq FOF_system_atomic_formula Source #
Methods (==) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool (/=) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool
Data FOF_system_atomic_formula Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_system_atomic_formula -> c FOF_system_atomic_formula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_system_atomic_formula toConstr :: FOF_system_atomic_formula -> Constr dataTypeOf :: FOF_system_atomic_formula -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_system_atomic_formula) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_system_atomic_formula) gmapT :: (forall b. Data b => b -> b) -> FOF_system_atomic_formula -> FOF_system_atomic_formula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_system_atomic_formula -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_system_atomic_formula -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_system_atomic_formula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_system_atomic_formula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_system_atomic_formula -> m FOF_system_atomic_formula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_system_atomic_formula -> m FOF_system_atomic_formula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_system_atomic_formula -> m FOF_system_atomic_formula
Ord FOF_system_atomic_formula Source #
Methods compare :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Ordering (<) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool (<=) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool (>) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool (>=) :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> Bool max :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> FOF_system_atomic_formula min :: FOF_system_atomic_formula -> FOF_system_atomic_formula -> FOF_system_atomic_formula
Show FOF_system_atomic_formula Source #
Methods showsPrec :: Int -> FOF_system_atomic_formula -> ShowS show :: FOF_system_atomic_formula -> String showList :: [FOF_system_atomic_formula] -> ShowS
GetRange FOF_system_atomic_formula Source #
Methods getRange :: FOF_system_atomic_formula -> Range Source # rangeSpan :: FOF_system_atomic_formula -> [Pos] Source #

data FOF_plain_term Source #

Constructors

FOFPT_constant Constant
FOFPT_functor TPTP_functor FOF_arguments

Instances

Eq FOF_plain_term Source #
Methods (==) :: FOF_plain_term -> FOF_plain_term -> Bool (/=) :: FOF_plain_term -> FOF_plain_term -> Bool
Data FOF_plain_term Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_plain_term -> c FOF_plain_term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_plain_term toConstr :: FOF_plain_term -> Constr dataTypeOf :: FOF_plain_term -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_plain_term) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_plain_term) gmapT :: (forall b. Data b => b -> b) -> FOF_plain_term -> FOF_plain_term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_plain_term -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_plain_term -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_plain_term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_plain_term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_plain_term -> m FOF_plain_term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_plain_term -> m FOF_plain_term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_plain_term -> m FOF_plain_term
Ord FOF_plain_term Source #
Methods compare :: FOF_plain_term -> FOF_plain_term -> Ordering (<) :: FOF_plain_term -> FOF_plain_term -> Bool (<=) :: FOF_plain_term -> FOF_plain_term -> Bool (>) :: FOF_plain_term -> FOF_plain_term -> Bool (>=) :: FOF_plain_term -> FOF_plain_term -> Bool max :: FOF_plain_term -> FOF_plain_term -> FOF_plain_term min :: FOF_plain_term -> FOF_plain_term -> FOF_plain_term
Show FOF_plain_term Source #
Methods showsPrec :: Int -> FOF_plain_term -> ShowS show :: FOF_plain_term -> String showList :: [FOF_plain_term] -> ShowS
GetRange FOF_plain_term Source #
Methods getRange :: FOF_plain_term -> Range Source # rangeSpan :: FOF_plain_term -> [Pos] Source #

data FOF_defined_term Source #

Constructors

FOFDT_term Defined_term
FOFDT_atomic FOF_defined_atomic_term

Instances

Eq FOF_defined_term Source #
Methods (==) :: FOF_defined_term -> FOF_defined_term -> Bool (/=) :: FOF_defined_term -> FOF_defined_term -> Bool
Data FOF_defined_term Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FOF_defined_term -> c FOF_defined_term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FOF_defined_term toConstr :: FOF_defined_term -> Constr dataTypeOf :: FOF_defined_term -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c FOF_defined_term) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FOF_defined_term) gmapT :: (forall b. Data b => b -> b) -> FOF_defined_term -> FOF_defined_term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_term -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FOF_defined_term -> r gmapQ :: (forall d. Data d => d -> u) -> FOF_defined_term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FOF_defined_term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FOF_defined_term -> m FOF_defined_term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_term -> m FOF_defined_term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FOF_defined_term -> m FOF_defined_term
Ord FOF_defined_term Source #
Methods compare :: FOF_defined_term -> FOF_defined_term -> Ordering (<) :: FOF_defined_term -> FOF_defined_term -> Bool (<=) :: FOF_defined_term -> FOF_defined_term -> Bool (>) :: FOF_defined_term -> FOF_defined_term -> Bool (>=) :: FOF_defined_term -> FOF_defined_term -> Bool max :: FOF_defined_term -> FOF_defined_term -> FOF_defined_term min :: FOF_defined_term -> FOF_defined_term -> FOF_defined_term
Show FOF_defined_term Source #
Methods showsPrec :: Int -> FOF_defined_term -> ShowS show :: FOF_defined_term -> String showList :: [FOF_defined_term] -> ShowS
GetRange FOF_defined_term Source #
Methods getRange :: FOF_defined_term -> Range Source # rangeSpan :: FOF_defined_term -> [Pos] Source #

data FOF_defined_atomic_term Source #

Constructors

FOFDAT_plain FOF_defined_plain_term

Instances

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