Copyright	(c) A. Tsogias DFKI Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Alexis.Tsogias@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

THF.As

Description

A Abstract Syntax for the TPTP-THF Input Syntax v5.1.0.2 taken from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html In addition the Syntax for THF0 taken from http://www.ags.uni-sb.de/~chris/papers/C25.pdf P. 15-16 has been added where needed.

Documentation

data TPTP_THF Source #

Constructors

TPTP_THF_Annotated_Formula
Fields nameAF :: Name formulaRoleAF :: FormulaRole thfFormulaAF :: THFFormula annotationsAF :: Annotations
TPTP_Include Include
TPTP_Comment Comment
TPTP_Defined_Comment DefinedComment
TPTP_System_Comment SystemComment
TPTP_Header [Comment]

Instances

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

Constructors

I_Include Token (Maybe NameList)

Instances

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

data Annotations Source #

Constructors

Annotations Source OptionalInfo
Null

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 FormulaRole Source #

Constructors

Axiom
Hypothesis
Definition
Assumption
Lemma
Theorem
Conjecture
Negated_Conjecture
Plain
Fi_Domain
Fi_Functors
Fi_Predicates
Type
Unknown

Instances

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

data THFFormula Source #

Constructors

TF_THF_Logic_Formula THFLogicFormula
TF_THF_Sequent THFSequent
T0F_THF_Typed_Const THFTypedConst

Instances

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

data THFLogicFormula Source #

Constructors

TLF_THF_Binary_Formula THFBinaryFormula
TLF_THF_Unitary_Formula THFUnitaryFormula
TLF_THF_Type_Formula THFTypeFormula
TLF_THF_Sub_Type THFSubType

Instances

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

data THFBinaryFormula Source #

Constructors

TBF_THF_Binary_Pair THFUnitaryFormula THFPairConnective THFUnitaryFormula
TBF_THF_Binary_Tuple THFBinaryTuple
TBF_THF_Binary_Type THFBinaryType

Instances

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

data THFBinaryTuple Source #

Constructors

TBT_THF_Or_Formula [THFUnitaryFormula]
TBT_THF_And_Formula [THFUnitaryFormula]
TBT_THF_Apply_Formula [THFUnitaryFormula]

Instances

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

data THFUnitaryFormula Source #

Constructors

TUF_THF_Quantified_Formula THFQuantifiedFormula
TUF_THF_Unary_Formula THFUnaryConnective THFLogicFormula
TUF_THF_Atom THFAtom
TUF_THF_Tuple THFTuple
TUF_THF_Conditional THFLogicFormula THFLogicFormula THFLogicFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
T0UF_THF_Abstraction THFVariableList THFUnitaryFormula

Instances

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

data THFQuantifiedFormula Source #

Constructors

TQF_THF_Quantified_Formula THFQuantifier THFVariableList THFUnitaryFormula
T0QF_THF_Quantified_Var Quantifier THFVariableList THFUnitaryFormula
T0QF_THF_Quantified_Novar THFQuantifier THFUnitaryFormula

Instances

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

type THFVariableList = [THFVariable] Source #

data THFVariable Source #

Constructors

TV_THF_Typed_Variable Token THFTopLevelType
TV_Variable Token

Instances

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

data THFTypedConst Source #

Constructors

T0TC_Typed_Const Constant THFTopLevelType
T0TC_THF_TypedConst_Par THFTypedConst

Instances

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

data THFTypeFormula Source #

Constructors

TTF_THF_Type_Formula THFTypeableFormula THFTopLevelType
TTF_THF_Typed_Const Constant THFTopLevelType

Instances

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

data THFTypeableFormula Source #

Constructors

TTyF_THF_Atom THFAtom
TTyF_THF_Tuple THFTuple
TTyF_THF_Logic_Formula THFLogicFormula

Instances

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

data THFSubType Source #

Constructors

TST_THF_Sub_Type Constant Constant

Instances

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

data THFTopLevelType Source #

Constructors

TTLT_THF_Logic_Formula THFLogicFormula
T0TLT_Constant Constant
T0TLT_Variable Token
T0TLT_Defined_Type DefinedType
T0TLT_System_Type Token
T0TLT_THF_Binary_Type THFBinaryType

Instances

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

data THFUnitaryType Source #

Constructors

TUT_THF_Unitary_Formula THFUnitaryFormula
T0UT_Constant Constant
T0UT_Variable Token
T0UT_Defined_Type DefinedType
T0UT_System_Type Token
T0UT_THF_Binary_Type_Par THFBinaryType

Instances

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

data THFBinaryType Source #

Constructors

TBT_THF_Mapping_Type [THFUnitaryType]
TBT_THF_Xprod_Type [THFUnitaryType]
TBT_THF_Union_Type [THFUnitaryType]
T0BT_THF_Binary_Type_Par THFBinaryType

Instances

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

data THFAtom Source #

Instances

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

type THFTuple = [THFLogicFormula] Source #

data THFSequent Source #

Constructors

TS_THF_Sequent THFTuple THFTuple
TS_THF_Sequent_Par THFSequent

Instances

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

data THFConnTerm Source #

Constructors

TCT_THF_Pair_Connective THFPairConnective
TCT_Assoc_Connective AssocConnective
TCT_THF_Unary_Connective THFUnaryConnective
T0CT_THF_Quantifier THFQuantifier

Instances

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

data THFQuantifier Source #

Constructors

TQ_ForAll
TQ_Exists
TQ_Lambda_Binder
TQ_Dependent_Product
TQ_Dependent_Sum
TQ_Indefinite_Description
TQ_Definite_Description
T0Q_PiForAll
T0Q_SigmaExists

Instances

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

data Quantifier Source #

Constructors

T0Q_ForAll
T0Q_Exists

Instances

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

data THFPairConnective Source #

Constructors

Infix_Equality
Infix_Inequality
Equivalent
Implication
IF
XOR
NOR
NAND

Instances

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

data THFUnaryConnective Source #

Constructors

Negation
PiForAll
SigmaExists

Instances

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

data AssocConnective Source #

Constructors

OR
AND

Instances

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

data DefinedType Source #

Constructors

DT_oType
DT_o
DT_iType
DT_i
DT_tType
DT_real
DT_rat
DT_int

Instances

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

data DefinedPlainFormula Source #

Constructors

DPF_Defined_Prop DefinedProp
DPF_Defined_Formula DefinedPred Arguments

Instances

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

data DefinedProp Source #

Constructors

DP_True
DP_False

Instances

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

data DefinedPred Source #

Constructors

Disrinct
Less
Lesseq
Greater
Greatereq
Is_int
Is_rat

Instances

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

data Term Source #

Constructors

T_Function_Term FunctionTerm
T_Variable Token

Instances

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

data FunctionTerm Source #

Constructors

FT_Plain_Term PlainTerm
FT_Defined_Term DefinedTerm
FT_System_Term SystemTerm

Instances

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

data PlainTerm Source #

Constructors

PT_Plain_Term AtomicWord Arguments
PT_Constant Constant

Instances

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

type Constant = AtomicWord Source #

data DefinedTerm Source #

Constructors

DT_Defined_Atom DefinedAtom
DT_Defined_Atomic_Term DefinedPlainTerm

Instances

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

data DefinedAtom Source #

Constructors

DA_Number Number
DA_Distinct_Object Token

Instances

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

data DefinedPlainTerm Source #

Constructors

DPT_Defined_Function DefinedFunctor Arguments
DPT_Defined_Constant DefinedFunctor

Instances

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

data DefinedFunctor Source #

Constructors

UMinus
Sum
Difference
Product
Quotient
Quotient_e
Quotient_t
Quotient_f
Remainder_e
Remainder_t
Remainder_f
Floor
Ceiling
Truncate
Round
To_int
To_rat
To_real

Instances

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

data SystemTerm Source #

Constructors

ST_System_Term Token Arguments
ST_System_Constant Token

Instances

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

type Arguments = [Term] Source #

data PrincipalSymbol Source #

Constructors

PS_Functor AtomicWord
PS_Variable Token

Instances

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

data Source Source #

Constructors

S_Dag_Source DagSource
S_Internal_Source IntroType OptionalInfo
S_External_Source ExternalSource
S_Sources [Source]
S_Unknown

Instances

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

data DagSource Source #

Constructors

DS_Name Name
DS_Inference_Record AtomicWord UsefulInfo [ParentInfo]

Instances

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

data ParentInfo Source #

Constructors

PI_Parent_Info Source (Maybe GeneralList)

Instances

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

data IntroType Source #

Constructors

IT_definition
IT_axiom_of_choice
IT_tautology
IT_assumption

Instances

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

data ExternalSource Source #

Constructors

ES_File_Source FileSource
ES_Theory TheoryName OptionalInfo
ES_Creator_Source AtomicWord OptionalInfo

Instances

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

data FileSource Source #

Constructors

FS_File Token (Maybe Name)

Instances

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

data TheoryName Source #

Constructors

Equality
Ac

Instances

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

type OptionalInfo = Maybe UsefulInfo Source #

type UsefulInfo = [InfoItem] Source #

data InfoItem Source #

Constructors

II_Formula_Item FormulaItem
II_Inference_Item InferenceItem
II_General_Function GeneralFunction

Instances

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

data FormulaItem Source #

Constructors

FI_Description_Item AtomicWord
FI_Iquote_Item AtomicWord

Instances

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

data InferenceItem Source #

Constructors

II_Inference_Status InferenceStatus
II_Assumptions_Record NameList
II_New_Symbol_Record AtomicWord [PrincipalSymbol]
II_Refutation FileSource

Instances

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

data InferenceStatus Source #

Constructors

IS_Status StatusValue
IS_Inference_Info AtomicWord AtomicWord GeneralList

Instances

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

data StatusValue Source #

Constructors

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Instances

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

type NameList = [Name] Source #

data GeneralTerm Source #

Constructors

GT_General_Data GeneralData
GT_General_Data_Term GeneralData GeneralTerm
GT_General_List GeneralList

Instances

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

data GeneralData Source #

Constructors

GD_Atomic_Word AtomicWord
GD_Variable Token
GD_Number Number
GD_Distinct_Object Token
GD_Formula_Data FormulaData
GD_Bind Token FormulaData
GD_General_Function GeneralFunction

Instances

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

data GeneralFunction Source #

Constructors

GF_General_Function AtomicWord GeneralTerms

Instances

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

data FormulaData Source #

Constructors

THF_Formula THFFormula

Instances

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

type GeneralList = GeneralTerms Source #

type GeneralTerms = [GeneralTerm] Source #

data Name Source #

Constructors

N_Atomic_Word AtomicWord
N_Integer Token
T0N_Unsigned_Integer Token

Instances

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

data AtomicWord Source #

Constructors

A_Lower_Word Token
A_Single_Quoted Token

Instances

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

data Number Source #

Constructors

Num_Integer Token
Num_Rational Token
Num_Real Token

Instances

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

TA_Term Term
TA_THF_Conn_Term THFConnTerm
TA_Defined_Type DefinedType
TA_Defined_Plain_Formula DefinedPlainFormula
TA_System_Type Token
TA_System_Atomic_Formula SystemTerm
T0A_Constant Constant
T0A_Defined_Constant Token
T0A_System_Constant Token
T0A_Variable Token

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc