Hets - the Heterogeneous Tool Set
Copyright(c) Eugen Kuksa University of Magdeburg 2017
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEugen Kuksa <kuksa@iks.cs.ovgu.de>
Stabilityprovisional
Portabilityportable
Safe HaskellNone

TPTP.AS

Description

Definition of abstract syntax for TPTP taken from [1]

References

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

Note: The implemented version is saved at TPTPDocumentsSyntaxBNF.html

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

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

Documentation

newtype BASIC_SPEC Source #

Constructors

Basic_spec [Annoted TPTP] 

Instances

Instances details
Eq BASIC_SPEC Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: BASIC_SPEC -> BASIC_SPEC -> Bool

(/=) :: BASIC_SPEC -> BASIC_SPEC -> Bool

Data BASIC_SPEC Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: BASIC_SPEC -> Constr

dataTypeOf :: BASIC_SPEC -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> BASIC_SPEC -> BASIC_SPEC

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

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

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

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

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

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

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

Ord BASIC_SPEC Source # 
Instance details

Defined in TPTP.AS

Show BASIC_SPEC Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> BASIC_SPEC -> ShowS

show :: BASIC_SPEC -> String

showList :: [BASIC_SPEC] -> ShowS

Generic BASIC_SPEC 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep BASIC_SPEC :: Type -> Type

Methods

from :: BASIC_SPEC -> Rep BASIC_SPEC x

to :: Rep BASIC_SPEC x -> BASIC_SPEC

Semigroup BASIC_SPEC 
Instance details

Defined in TPTP.Logic_TPTP

Methods

(<>) :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC #

sconcat :: NonEmpty BASIC_SPEC -> BASIC_SPEC

stimes :: Integral b => b -> BASIC_SPEC -> BASIC_SPEC

Monoid BASIC_SPEC 
Instance details

Defined in TPTP.Logic_TPTP

GetRange BASIC_SPEC Source # 
Instance details

Defined in TPTP.AS

FromJSON BASIC_SPEC 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser BASIC_SPEC

parseJSONList :: Value -> Parser [BASIC_SPEC]

ToJSON BASIC_SPEC 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: BASIC_SPEC -> Value

toEncoding :: BASIC_SPEC -> Encoding

toJSONList :: [BASIC_SPEC] -> Value

toEncodingList :: [BASIC_SPEC] -> Encoding

ShATermConvertible BASIC_SPEC 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_SPEC] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC])

Pretty BASIC_SPEC Source # 
Instance details

Defined in TPTP.Pretty

ProjectSublogic Sublogic BASIC_SPEC Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic BASIC_SPEC Source # 
Instance details

Defined in TPTP.Logic_TPTP

Syntax TPTP BASIC_SPEC Symbol () () Source # 
Instance details

Defined in TPTP.Logic_TPTP

StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source #

convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: TPTP -> Symbol -> () Source #

id_to_raw :: TPTP -> Id -> () Source #

matches :: TPTP -> Symbol -> () -> Bool Source #

empty_signature :: TPTP -> Sign Source #

add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source #

signature_union :: TPTP -> Sign -> Sign -> Result Sign Source #

signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source #

intersection :: TPTP -> Sign -> Sign -> Result Sign Source #

final_union :: TPTP -> Sign -> Sign -> Result Sign Source #

morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: TPTP -> Sign -> Sign -> Bool Source #

subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source #

generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: TPTP -> Morphism -> Bool Source #

is_injective :: TPTP -> Morphism -> Bool Source #

theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #

type Rep BASIC_SPEC 
Instance details

Defined in TPTP.ATC_TPTP

type Rep BASIC_SPEC = D1 ('MetaData "BASIC_SPEC" "TPTP.AS" "main" 'True) (C1 ('MetaCons "Basic_spec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted TPTP])))

newtype TPTP Source #

Constructors

TPTP [TPTP_input] 

Instances

Instances details
Eq TPTP Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: TPTP -> TPTP -> Bool

(/=) :: TPTP -> TPTP -> Bool

Data TPTP Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TPTP -> Constr

dataTypeOf :: TPTP -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TPTP -> TPTP

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

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

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

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

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

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

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

Ord TPTP Source # 
Instance details

Defined in TPTP.AS

Methods

compare :: TPTP -> TPTP -> Ordering

(<) :: TPTP -> TPTP -> Bool

(<=) :: TPTP -> TPTP -> Bool

(>) :: TPTP -> TPTP -> Bool

(>=) :: TPTP -> TPTP -> Bool

max :: TPTP -> TPTP -> TPTP

min :: TPTP -> TPTP -> TPTP

Show TPTP Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TPTP -> ShowS

show :: TPTP -> String

showList :: [TPTP] -> ShowS

Generic TPTP 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TPTP :: Type -> Type

Methods

from :: TPTP -> Rep TPTP x

to :: Rep TPTP x -> TPTP

GetRange TPTP Source # 
Instance details

Defined in TPTP.AS

FromJSON TPTP 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TPTP

parseJSONList :: Value -> Parser [TPTP]

ToJSON TPTP 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TPTP -> Value

toEncoding :: TPTP -> Encoding

toJSONList :: [TPTP] -> Value

toEncodingList :: [TPTP] -> Encoding

ShATermConvertible TPTP 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TPTP -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPTP] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP])

Pretty TPTP Source # 
Instance details

Defined in TPTP.Pretty

Methods

pretty :: TPTP -> Doc Source #

pretties :: [TPTP] -> Doc Source #

type Rep TPTP 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TPTP = D1 ('MetaData "TPTP" "TPTP.AS" "main" 'True) (C1 ('MetaCons "TPTP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TPTP_input])))

data TPTP_input Source #

Instances

Instances details
Eq TPTP_input Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: TPTP_input -> TPTP_input -> Bool

(/=) :: TPTP_input -> TPTP_input -> Bool

Data TPTP_input Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TPTP_input -> Constr

dataTypeOf :: TPTP_input -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TPTP_input -> TPTP_input

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

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

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

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

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

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

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

Ord TPTP_input Source # 
Instance details

Defined in TPTP.AS

Show TPTP_input Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TPTP_input -> ShowS

show :: TPTP_input -> String

showList :: [TPTP_input] -> ShowS

Generic TPTP_input 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TPTP_input :: Type -> Type

Methods

from :: TPTP_input -> Rep TPTP_input x

to :: Rep TPTP_input x -> TPTP_input

GetRange TPTP_input Source # 
Instance details

Defined in TPTP.AS

FromJSON TPTP_input 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TPTP_input

parseJSONList :: Value -> Parser [TPTP_input]

ToJSON TPTP_input 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TPTP_input -> Value

toEncoding :: TPTP_input -> Encoding

toJSONList :: [TPTP_input] -> Value

toEncodingList :: [TPTP_input] -> Encoding

ShATermConvertible TPTP_input 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TPTP_input -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPTP_input] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP_input)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP_input])

Pretty TPTP_input Source # 
Instance details

Defined in TPTP.Pretty

type Rep TPTP_input 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TPTP_input = D1 ('MetaData "TPTP_input" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "Annotated_formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotated_formula)) :+: C1 ('MetaCons "TPTP_include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Include))) :+: (C1 ('MetaCons "TPTP_comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comment)) :+: (C1 ('MetaCons "TPTP_defined_comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedComment)) :+: C1 ('MetaCons "TPTP_system_comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SystemComment)))))

data Comment Source #

Instances

Instances details
Eq Comment Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: Comment -> Comment -> Bool

(/=) :: Comment -> Comment -> Bool

Data Comment Source # 
Instance details

Defined in TPTP.AS

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 :: forall r r'. (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 # 
Instance details

Defined in TPTP.AS

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 # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> Comment -> ShowS

show :: Comment -> String

showList :: [Comment] -> ShowS

Generic Comment 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep Comment :: Type -> Type

Methods

from :: Comment -> Rep Comment x

to :: Rep Comment x -> Comment

GetRange Comment Source # 
Instance details

Defined in TPTP.AS

FromJSON Comment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser Comment

parseJSONList :: Value -> Parser [Comment]

ToJSON Comment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: Comment -> Value

toEncoding :: Comment -> Encoding

toJSONList :: [Comment] -> Value

toEncodingList :: [Comment] -> Encoding

ShATermConvertible Comment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> Comment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Comment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Comment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Comment])

Pretty Comment Source # 
Instance details

Defined in TPTP.Pretty

type Rep Comment 
Instance details

Defined in TPTP.ATC_TPTP

type Rep Comment = D1 ('MetaData "Comment" "TPTP.AS" "main" 'False) (C1 ('MetaCons "Comment_line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Comment_block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data DefinedComment Source #

Instances

Instances details
Eq DefinedComment Source # 
Instance details

Defined in TPTP.AS

Data DefinedComment Source # 
Instance details

Defined in TPTP.AS

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 :: forall r r'. (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 # 
Instance details

Defined in TPTP.AS

Show DefinedComment Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> DefinedComment -> ShowS

show :: DefinedComment -> String

showList :: [DefinedComment] -> ShowS

Generic DefinedComment 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep DefinedComment :: Type -> Type

GetRange DefinedComment Source # 
Instance details

Defined in TPTP.AS

FromJSON DefinedComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser DefinedComment

parseJSONList :: Value -> Parser [DefinedComment]

ToJSON DefinedComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: DefinedComment -> Value

toEncoding :: DefinedComment -> Encoding

toJSONList :: [DefinedComment] -> Value

toEncodingList :: [DefinedComment] -> Encoding

ShATermConvertible DefinedComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> DefinedComment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DefinedComment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedComment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedComment])

Pretty DefinedComment Source # 
Instance details

Defined in TPTP.Pretty

type Rep DefinedComment 
Instance details

Defined in TPTP.ATC_TPTP

type Rep DefinedComment = D1 ('MetaData "DefinedComment" "TPTP.AS" "main" 'False) (C1 ('MetaCons "Defined_comment_line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Defined_comment_block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data SystemComment Source #

Instances

Instances details
Eq SystemComment Source # 
Instance details

Defined in TPTP.AS

Data SystemComment Source # 
Instance details

Defined in TPTP.AS

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 :: forall r r'. (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 # 
Instance details

Defined in TPTP.AS

Show SystemComment Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> SystemComment -> ShowS

show :: SystemComment -> String

showList :: [SystemComment] -> ShowS

Generic SystemComment 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep SystemComment :: Type -> Type

GetRange SystemComment Source # 
Instance details

Defined in TPTP.AS

FromJSON SystemComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser SystemComment

parseJSONList :: Value -> Parser [SystemComment]

ToJSON SystemComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: SystemComment -> Value

toEncoding :: SystemComment -> Encoding

toJSONList :: [SystemComment] -> Value

toEncodingList :: [SystemComment] -> Encoding

ShATermConvertible SystemComment 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> SystemComment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SystemComment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SystemComment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SystemComment])

Pretty SystemComment Source # 
Instance details

Defined in TPTP.Pretty

type Rep SystemComment 
Instance details

Defined in TPTP.ATC_TPTP

type Rep SystemComment = D1 ('MetaData "SystemComment" "TPTP.AS" "main" 'False) (C1 ('MetaCons "System_comment_line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "System_comment_block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data Annotated_formula Source #

Instances

Instances details
Eq Annotated_formula Source # 
Instance details

Defined in TPTP.AS

Data Annotated_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: Annotated_formula -> Constr

dataTypeOf :: Annotated_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Annotated_formula -> Annotated_formula

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

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

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

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

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

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

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

Ord Annotated_formula Source # 
Instance details

Defined in TPTP.AS

Show Annotated_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> Annotated_formula -> ShowS

show :: Annotated_formula -> String

showList :: [Annotated_formula] -> ShowS

Generic Annotated_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep Annotated_formula :: Type -> Type

GetRange Annotated_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON Annotated_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser Annotated_formula

parseJSONList :: Value -> Parser [Annotated_formula]

ToJSON Annotated_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible Annotated_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> Annotated_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Annotated_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotated_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annotated_formula])

Pretty Annotated_formula Source # 
Instance details

Defined in TPTP.Pretty

ProjectSublogic Sublogic Sentence Source # 
Instance details

Defined in TPTP.Logic_TPTP

MinSublogic Sublogic Sentence Source # 
Instance details

Defined in TPTP.Logic_TPTP

Sentences TPTP Sentence Sign Morphism Symbol Source # 
Instance details

Defined in TPTP.Logic_TPTP

StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol () Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

basic_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: TPTP -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: TPTP -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: TPTP -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: TPTP -> Sign -> [()] -> Result [()] Source #

convertTheory :: TPTP -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

ensures_amalgamability :: TPTP -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: TPTP -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: TPTP -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: TPTP -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: TPTP -> Symbol -> () Source #

id_to_raw :: TPTP -> Id -> () Source #

matches :: TPTP -> Symbol -> () -> Bool Source #

empty_signature :: TPTP -> Sign Source #

add_symb_to_sign :: TPTP -> Sign -> Symbol -> Result Sign Source #

signature_union :: TPTP -> Sign -> Sign -> Result Sign Source #

signatureDiff :: TPTP -> Sign -> Sign -> Result Sign Source #

intersection :: TPTP -> Sign -> Sign -> Result Sign Source #

final_union :: TPTP -> Sign -> Sign -> Result Sign Source #

morphism_union :: TPTP -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: TPTP -> Sign -> Sign -> Bool Source #

subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism Source #

generated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: TPTP -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: TPTP -> EndoMap () -> Sign -> Result Morphism Source #

induced_from_to_morphism :: TPTP -> EndoMap () -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: TPTP -> Morphism -> Bool Source #

is_injective :: TPTP -> Morphism -> Bool Source #

theory_to_taxonomy :: TPTP -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: TPTP -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: TPTP -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: TPTP -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree Source # 
Instance details

Defined in TPTP.Logic_TPTP

Methods

parse_basic_sen :: TPTP -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: TPTP -> Stability Source #

data_logic :: TPTP -> Maybe AnyLogic Source #

top_sublogic :: TPTP -> Sublogic Source #

all_sublogics :: TPTP -> [Sublogic] Source #

bottomSublogic :: TPTP -> Maybe Sublogic Source #

sublogicDimensions :: TPTP -> [[Sublogic]] Source #

parseSublogic :: TPTP -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: TPTP -> Sublogic -> Sign -> Morphism Source #

provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree] Source #

default_prover :: TPTP -> String Source #

cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree] Source #

conservativityCheck :: TPTP -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: TPTP -> ProofTree Source #

syntaxTable :: TPTP -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: TPTP -> Maybe OMCD Source #

export_symToOmdoc :: TPTP -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: TPTP -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: TPTP -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: TPTP -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: TPTP -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

sublogicOfTheo :: TPTP -> (Sign, [Sentence]) -> Sublogic Source #

type Rep Annotated_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep Annotated_formula = D1 ('MetaData "Annotated_formula" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "AF_THF_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_annotated)) :+: (C1 ('MetaCons "AF_TFX_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFX_annotated)) :+: C1 ('MetaCons "AF_TFF_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_annotated)))) :+: ((C1 ('MetaCons "AF_TCF_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCF_annotated)) :+: C1 ('MetaCons "AF_FOF_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FOF_annotated))) :+: (C1 ('MetaCons "AF_CNF_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CNF_annotated)) :+: C1 ('MetaCons "AF_TPI_Annotated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPI_annotated)))))

data TPI_annotated Source #

Instances

Instances details
Eq TPI_annotated Source # 
Instance details

Defined in TPTP.AS

Data TPI_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TPI_annotated -> Constr

dataTypeOf :: TPI_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TPI_annotated -> TPI_annotated

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

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

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

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

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

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

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

Ord TPI_annotated Source # 
Instance details

Defined in TPTP.AS

Show TPI_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TPI_annotated -> ShowS

show :: TPI_annotated -> String

showList :: [TPI_annotated] -> ShowS

Generic TPI_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TPI_annotated :: Type -> Type

GetRange TPI_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON TPI_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TPI_annotated

parseJSONList :: Value -> Parser [TPI_annotated]

ToJSON TPI_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TPI_annotated -> Value

toEncoding :: TPI_annotated -> Encoding

toJSONList :: [TPI_annotated] -> Value

toEncodingList :: [TPI_annotated] -> Encoding

ShATermConvertible TPI_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TPI_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPI_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPI_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPI_annotated])

Pretty TPI_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep TPI_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TPI_annotated = D1 ('MetaData "TPI_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TPI_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPI_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data THF_annotated Source #

Instances

Instances details
Eq THF_annotated Source # 
Instance details

Defined in TPTP.AS

Data THF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_annotated -> Constr

dataTypeOf :: THF_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_annotated -> THF_annotated

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

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

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

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

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

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

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

Ord THF_annotated Source # 
Instance details

Defined in TPTP.AS

Show THF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_annotated -> ShowS

show :: THF_annotated -> String

showList :: [THF_annotated] -> ShowS

Generic THF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_annotated :: Type -> Type

GetRange THF_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_annotated

parseJSONList :: Value -> Parser [THF_annotated]

ToJSON THF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_annotated -> Value

toEncoding :: THF_annotated -> Encoding

toJSONList :: [THF_annotated] -> Value

toEncodingList :: [THF_annotated] -> Encoding

ShATermConvertible THF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_annotated])

Pretty THF_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_annotated = D1 ('MetaData "THF_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data TFX_annotated Source #

Instances

Instances details
Eq TFX_annotated Source # 
Instance details

Defined in TPTP.AS

Data TFX_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFX_annotated -> Constr

dataTypeOf :: TFX_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFX_annotated -> TFX_annotated

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

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

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

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

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

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

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

Ord TFX_annotated Source # 
Instance details

Defined in TPTP.AS

Show TFX_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFX_annotated -> ShowS

show :: TFX_annotated -> String

showList :: [TFX_annotated] -> ShowS

Generic TFX_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFX_annotated :: Type -> Type

GetRange TFX_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON TFX_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFX_annotated

parseJSONList :: Value -> Parser [TFX_annotated]

ToJSON TFX_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TFX_annotated -> Value

toEncoding :: TFX_annotated -> Encoding

toJSONList :: [TFX_annotated] -> Value

toEncodingList :: [TFX_annotated] -> Encoding

ShATermConvertible TFX_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFX_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_annotated])

Pretty TFX_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFX_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFX_annotated = D1 ('MetaData "TFX_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFX_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFX_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data TFF_annotated Source #

Instances

Instances details
Eq TFF_annotated Source # 
Instance details

Defined in TPTP.AS

Data TFF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFF_annotated -> Constr

dataTypeOf :: TFF_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFF_annotated -> TFF_annotated

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

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

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

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

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

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

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

Ord TFF_annotated Source # 
Instance details

Defined in TPTP.AS

Show TFF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFF_annotated -> ShowS

show :: TFF_annotated -> String

showList :: [TFF_annotated] -> ShowS

Generic TFF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFF_annotated :: Type -> Type

GetRange TFF_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON TFF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFF_annotated

parseJSONList :: Value -> Parser [TFF_annotated]

ToJSON TFF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TFF_annotated -> Value

toEncoding :: TFF_annotated -> Encoding

toJSONList :: [TFF_annotated] -> Value

toEncodingList :: [TFF_annotated] -> Encoding

ShATermConvertible TFF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_annotated])

Pretty TFF_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFF_annotated = D1 ('MetaData "TFF_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFF_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data TCF_annotated Source #

Instances

Instances details
Eq TCF_annotated Source # 
Instance details

Defined in TPTP.AS

Data TCF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TCF_annotated -> Constr

dataTypeOf :: TCF_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TCF_annotated -> TCF_annotated

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

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

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

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

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

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

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

Ord TCF_annotated Source # 
Instance details

Defined in TPTP.AS

Show TCF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TCF_annotated -> ShowS

show :: TCF_annotated -> String

showList :: [TCF_annotated] -> ShowS

Generic TCF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TCF_annotated :: Type -> Type

GetRange TCF_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON TCF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TCF_annotated

parseJSONList :: Value -> Parser [TCF_annotated]

ToJSON TCF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TCF_annotated -> Value

toEncoding :: TCF_annotated -> Encoding

toJSONList :: [TCF_annotated] -> Value

toEncodingList :: [TCF_annotated] -> Encoding

ShATermConvertible TCF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TCF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TCF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TCF_annotated])

Pretty TCF_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep TCF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TCF_annotated = D1 ('MetaData "TCF_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TCF_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCF_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data FOF_annotated Source #

Instances

Instances details
Eq FOF_annotated Source # 
Instance details

Defined in TPTP.AS

Data FOF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: FOF_annotated -> Constr

dataTypeOf :: FOF_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> FOF_annotated -> FOF_annotated

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

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

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

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

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

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

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

Ord FOF_annotated Source # 
Instance details

Defined in TPTP.AS

Show FOF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> FOF_annotated -> ShowS

show :: FOF_annotated -> String

showList :: [FOF_annotated] -> ShowS

Generic FOF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep FOF_annotated :: Type -> Type

GetRange FOF_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON FOF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser FOF_annotated

parseJSONList :: Value -> Parser [FOF_annotated]

ToJSON FOF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: FOF_annotated -> Value

toEncoding :: FOF_annotated -> Encoding

toJSONList :: [FOF_annotated] -> Value

toEncodingList :: [FOF_annotated] -> Encoding

ShATermConvertible FOF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> FOF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_annotated])

Pretty FOF_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep FOF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep FOF_annotated = D1 ('MetaData "FOF_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "FOF_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FOF_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

data CNF_annotated Source #

Instances

Instances details
Eq CNF_annotated Source # 
Instance details

Defined in TPTP.AS

Data CNF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: CNF_annotated -> Constr

dataTypeOf :: CNF_annotated -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> CNF_annotated -> CNF_annotated

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

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

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

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

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

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

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

Ord CNF_annotated Source # 
Instance details

Defined in TPTP.AS

Show CNF_annotated Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> CNF_annotated -> ShowS

show :: CNF_annotated -> String

showList :: [CNF_annotated] -> ShowS

Generic CNF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep CNF_annotated :: Type -> Type

GetRange CNF_annotated Source # 
Instance details

Defined in TPTP.AS

FromJSON CNF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser CNF_annotated

parseJSONList :: Value -> Parser [CNF_annotated]

ToJSON CNF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: CNF_annotated -> Value

toEncoding :: CNF_annotated -> Encoding

toJSONList :: [CNF_annotated] -> Value

toEncodingList :: [CNF_annotated] -> Encoding

ShATermConvertible CNF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> CNF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CNF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CNF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CNF_annotated])

Pretty CNF_annotated Source # 
Instance details

Defined in TPTP.Pretty

type Rep CNF_annotated 
Instance details

Defined in TPTP.ATC_TPTP

type Rep CNF_annotated = D1 ('MetaData "CNF_annotated" "TPTP.AS" "main" 'False) (C1 ('MetaCons "CNF_annotated" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Formula_role)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CNF_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))))

newtype Annotations Source #

Constructors

Annotations (Maybe (Source, Optional_info)) 

Instances

Instances details
Eq Annotations Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: Annotations -> Annotations -> Bool

(/=) :: Annotations -> Annotations -> Bool

Data Annotations Source # 
Instance details

Defined in TPTP.AS

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 :: forall r r'. (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 # 
Instance details

Defined in TPTP.AS

Show Annotations Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> Annotations -> ShowS

show :: Annotations -> String

showList :: [Annotations] -> ShowS

Generic Annotations 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep Annotations :: Type -> Type

Methods

from :: Annotations -> Rep Annotations x

to :: Rep Annotations x -> Annotations

GetRange Annotations Source # 
Instance details

Defined in TPTP.AS

FromJSON Annotations 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser Annotations

parseJSONList :: Value -> Parser [Annotations]

ToJSON Annotations 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: Annotations -> Value

toEncoding :: Annotations -> Encoding

toJSONList :: [Annotations] -> Value

toEncodingList :: [Annotations] -> Encoding

ShATermConvertible Annotations 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> Annotations -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Annotations] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotations)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annotations])

Pretty Annotations Source # 
Instance details

Defined in TPTP.Pretty

type Rep Annotations 
Instance details

Defined in TPTP.ATC_TPTP

type Rep Annotations = D1 ('MetaData "Annotations" "TPTP.AS" "main" 'True) (C1 ('MetaCons "Annotations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Source, Optional_info)))))

data Formula_role Source #

Instances

Instances details
Eq Formula_role Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: Formula_role -> Formula_role -> Bool

(/=) :: Formula_role -> Formula_role -> Bool

Data Formula_role Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: Formula_role -> Constr

dataTypeOf :: Formula_role -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Formula_role -> Formula_role

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

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

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

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

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

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

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

Ord Formula_role Source # 
Instance details

Defined in TPTP.AS

Show Formula_role Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> Formula_role -> ShowS

show :: Formula_role -> String

showList :: [Formula_role] -> ShowS

Generic Formula_role 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep Formula_role :: Type -> Type

GetRange Formula_role Source # 
Instance details

Defined in TPTP.AS

FromJSON Formula_role 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser Formula_role

parseJSONList :: Value -> Parser [Formula_role]

ToJSON Formula_role 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: Formula_role -> Value

toEncoding :: Formula_role -> Encoding

toJSONList :: [Formula_role] -> Value

toEncodingList :: [Formula_role] -> Encoding

ShATermConvertible Formula_role 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> Formula_role -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Formula_role] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Formula_role)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Formula_role])

Pretty Formula_role Source # 
Instance details

Defined in TPTP.Pretty

type Rep Formula_role 
Instance details

Defined in TPTP.ATC_TPTP

type Rep Formula_role = D1 ('MetaData "Formula_role" "TPTP.AS" "main" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hypothesis" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Definition" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Assumption" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Lemma" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Theorem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Corollary" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Conjecture" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Negated_conjecture" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Plain" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Type" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_domain" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Fi_functors" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_predicates" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Other_formula_role" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))))))

data THF_formula Source #

Instances

Instances details
Eq THF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_formula -> THF_formula -> Bool

(/=) :: THF_formula -> THF_formula -> Bool

Data THF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_formula -> Constr

dataTypeOf :: THF_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_formula -> THF_formula

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

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

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

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

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

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

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

Ord THF_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_formula -> ShowS

show :: THF_formula -> String

showList :: [THF_formula] -> ShowS

Generic THF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_formula :: Type -> Type

Methods

from :: THF_formula -> Rep THF_formula x

to :: Rep THF_formula x -> THF_formula

GetRange THF_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_formula

parseJSONList :: Value -> Parser [THF_formula]

ToJSON THF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_formula -> Value

toEncoding :: THF_formula -> Encoding

toJSONList :: [THF_formula] -> Value

toEncodingList :: [THF_formula] -> Encoding

ShATermConvertible THF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_formula])

Pretty THF_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_formula = D1 ('MetaData "THF_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFF_logic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula)) :+: C1 ('MetaCons "THFF_sequent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_sequent)))

data THF_logic_formula Source #

Instances

Instances details
Eq THF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_logic_formula -> Constr

dataTypeOf :: THF_logic_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_logic_formula -> THF_logic_formula

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

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

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

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

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

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

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

Ord THF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_logic_formula -> ShowS

show :: THF_logic_formula -> String

showList :: [THF_logic_formula] -> ShowS

Generic THF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_logic_formula :: Type -> Type

GetRange THF_logic_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_logic_formula

parseJSONList :: Value -> Parser [THF_logic_formula]

ToJSON THF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_logic_formula])

Pretty THF_logic_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_logic_formula = D1 ('MetaData "THF_logic_formula" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "THFLF_binary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_binary_formula)) :+: C1 ('MetaCons "THFLF_unitary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula))) :+: (C1 ('MetaCons "THFLF_type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_type_formula)) :+: C1 ('MetaCons "THFLF_subtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_subtype))))

data THF_binary_formula Source #

Instances

Instances details
Eq THF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_binary_formula -> Constr

dataTypeOf :: THF_binary_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_binary_formula -> THF_binary_formula

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

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

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

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

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

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

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

Ord THF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_binary_formula -> ShowS

show :: THF_binary_formula -> String

showList :: [THF_binary_formula] -> ShowS

Generic THF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_binary_formula :: Type -> Type

GetRange THF_binary_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_binary_formula

parseJSONList :: Value -> Parser [THF_binary_formula]

ToJSON THF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_binary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_formula])

Pretty THF_binary_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_binary_formula = D1 ('MetaData "THF_binary_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFBF_pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_binary_pair)) :+: C1 ('MetaCons "THFBF_tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_binary_tuple)))

data THF_binary_pair Source #

Instances

Instances details
Eq THF_binary_pair Source # 
Instance details

Defined in TPTP.AS

Data THF_binary_pair Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_binary_pair -> Constr

dataTypeOf :: THF_binary_pair -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_binary_pair -> THF_binary_pair

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

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

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

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

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

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

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

Ord THF_binary_pair Source # 
Instance details

Defined in TPTP.AS

Show THF_binary_pair Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_binary_pair -> ShowS

show :: THF_binary_pair -> String

showList :: [THF_binary_pair] -> ShowS

Generic THF_binary_pair 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_binary_pair :: Type -> Type

GetRange THF_binary_pair Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_binary_pair 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_binary_pair

parseJSONList :: Value -> Parser [THF_binary_pair]

ToJSON THF_binary_pair 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_binary_pair -> Value

toEncoding :: THF_binary_pair -> Encoding

toJSONList :: [THF_binary_pair] -> Value

toEncodingList :: [THF_binary_pair] -> Encoding

ShATermConvertible THF_binary_pair 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_binary_pair -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_pair] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_pair)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_pair])

Pretty THF_binary_pair Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_binary_pair 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_binary_pair = D1 ('MetaData "THF_binary_pair" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_binary_pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_pair_connective) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula))))

data THF_binary_tuple Source #

Instances

Instances details
Eq THF_binary_tuple Source # 
Instance details

Defined in TPTP.AS

Data THF_binary_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_binary_tuple -> Constr

dataTypeOf :: THF_binary_tuple -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_binary_tuple -> THF_binary_tuple

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

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

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

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

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

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

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

Ord THF_binary_tuple Source # 
Instance details

Defined in TPTP.AS

Show THF_binary_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_binary_tuple -> ShowS

show :: THF_binary_tuple -> String

showList :: [THF_binary_tuple] -> ShowS

Generic THF_binary_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_binary_tuple :: Type -> Type

GetRange THF_binary_tuple Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_binary_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_binary_tuple

parseJSONList :: Value -> Parser [THF_binary_tuple]

ToJSON THF_binary_tuple 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_binary_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_binary_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_tuple])

Pretty THF_binary_tuple Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_binary_tuple 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_binary_tuple = D1 ('MetaData "THF_binary_tuple" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFBT_or" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_or_formula)) :+: (C1 ('MetaCons "THFBT_and" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_and_formula)) :+: C1 ('MetaCons "THFBT_apply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_apply_formula))))

data THF_unitary_formula Source #

Instances

Instances details
Eq THF_unitary_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_unitary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_unitary_formula -> Constr

dataTypeOf :: THF_unitary_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_unitary_formula -> THF_unitary_formula

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

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

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

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

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

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

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

Ord THF_unitary_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_unitary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_unitary_formula -> ShowS

show :: THF_unitary_formula -> String

showList :: [THF_unitary_formula] -> ShowS

Generic THF_unitary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_unitary_formula :: Type -> Type

GetRange THF_unitary_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_unitary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_unitary_formula

parseJSONList :: Value -> Parser [THF_unitary_formula]

ToJSON THF_unitary_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_unitary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unitary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unitary_formula])

Pretty THF_unitary_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_unitary_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_unitary_formula = D1 ('MetaData "THF_unitary_formula" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "THFUF_quantified" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_quantified_formula)) :+: (C1 ('MetaCons "THFUF_unary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unary_formula)) :+: C1 ('MetaCons "THFUF_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_atom)))) :+: ((C1 ('MetaCons "THFUF_conditional" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_conditional)) :+: C1 ('MetaCons "THFUF_let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let))) :+: (C1 ('MetaCons "THFUF_tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_tuple)) :+: C1 ('MetaCons "THFUF_logic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula)))))

data THF_quantified_formula Source #

Instances

Instances details
Eq THF_quantified_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_quantified_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_quantified_formula -> Constr

dataTypeOf :: THF_quantified_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_quantified_formula -> THF_quantified_formula

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

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

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

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

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

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

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

Ord THF_quantified_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_quantified_formula Source # 
Instance details

Defined in TPTP.AS

Generic THF_quantified_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_quantified_formula :: Type -> Type

GetRange THF_quantified_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_quantified_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_quantified_formula

parseJSONList :: Value -> Parser [THF_quantified_formula]

ToJSON THF_quantified_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_quantified_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_quantified_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_quantified_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantified_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_quantified_formula])

Pretty THF_quantified_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_quantified_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_quantified_formula = D1 ('MetaData "THF_quantified_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_quantified_formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_quantification) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula)))

data THF_quantification Source #

Instances

Instances details
Eq THF_quantification Source # 
Instance details

Defined in TPTP.AS

Data THF_quantification Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_quantification -> Constr

dataTypeOf :: THF_quantification -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_quantification -> THF_quantification

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

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

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

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

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

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

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

Ord THF_quantification Source # 
Instance details

Defined in TPTP.AS

Show THF_quantification Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_quantification -> ShowS

show :: THF_quantification -> String

showList :: [THF_quantification] -> ShowS

Generic THF_quantification 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_quantification :: Type -> Type

GetRange THF_quantification Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_quantification 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_quantification

parseJSONList :: Value -> Parser [THF_quantification]

ToJSON THF_quantification 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_quantification 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_quantification -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_quantification] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantification)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_quantification])

Pretty THF_quantification Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_quantification 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_quantification = D1 ('MetaData "THF_quantification" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_quantification" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_quantifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_variable_list)))

data THF_variable Source #

Instances

Instances details
Eq THF_variable Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_variable -> THF_variable -> Bool

(/=) :: THF_variable -> THF_variable -> Bool

Data THF_variable Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_variable -> Constr

dataTypeOf :: THF_variable -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_variable -> THF_variable

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

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

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

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

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

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

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

Ord THF_variable Source # 
Instance details

Defined in TPTP.AS

Show THF_variable Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_variable -> ShowS

show :: THF_variable -> String

showList :: [THF_variable] -> ShowS

Generic THF_variable 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_variable :: Type -> Type

GetRange THF_variable Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_variable 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_variable

parseJSONList :: Value -> Parser [THF_variable]

ToJSON THF_variable 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_variable -> Value

toEncoding :: THF_variable -> Encoding

toJSONList :: [THF_variable] -> Value

toEncodingList :: [THF_variable] -> Encoding

ShATermConvertible THF_variable 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_variable])

Pretty THF_variable Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_variable 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_variable = D1 ('MetaData "THF_variable" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFV_typed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_typed_variable)) :+: C1 ('MetaCons "THFV_variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Variable)))

data THF_typed_variable Source #

Instances

Instances details
Eq THF_typed_variable Source # 
Instance details

Defined in TPTP.AS

Data THF_typed_variable Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_typed_variable -> Constr

dataTypeOf :: THF_typed_variable -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_typed_variable -> THF_typed_variable

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

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

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

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

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

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

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

Ord THF_typed_variable Source # 
Instance details

Defined in TPTP.AS

Show THF_typed_variable Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_typed_variable -> ShowS

show :: THF_typed_variable -> String

showList :: [THF_typed_variable] -> ShowS

Generic THF_typed_variable 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_typed_variable :: Type -> Type

GetRange THF_typed_variable Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_typed_variable 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_typed_variable

parseJSONList :: Value -> Parser [THF_typed_variable]

ToJSON THF_typed_variable 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_typed_variable 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_typed_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_typed_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typed_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_typed_variable])

Pretty THF_typed_variable Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_typed_variable 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_typed_variable = D1 ('MetaData "THF_typed_variable" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_typed_variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Variable) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_top_level_type)))

data THF_unary_formula Source #

Instances

Instances details
Eq THF_unary_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_unary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_unary_formula -> Constr

dataTypeOf :: THF_unary_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_unary_formula -> THF_unary_formula

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

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

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

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

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

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

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

Ord THF_unary_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_unary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_unary_formula -> ShowS

show :: THF_unary_formula -> String

showList :: [THF_unary_formula] -> ShowS

Generic THF_unary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_unary_formula :: Type -> Type

GetRange THF_unary_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_unary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_unary_formula

parseJSONList :: Value -> Parser [THF_unary_formula]

ToJSON THF_unary_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_unary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_unary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unary_formula])

Pretty THF_unary_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_unary_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_unary_formula = D1 ('MetaData "THF_unary_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_unary_formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unary_connective) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula)))

data THF_atom Source #

Instances

Instances details
Eq THF_atom Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_atom -> THF_atom -> Bool

(/=) :: THF_atom -> THF_atom -> Bool

Data THF_atom Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_atom -> Constr

dataTypeOf :: THF_atom -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_atom -> THF_atom

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

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

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

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

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

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

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

Ord THF_atom Source # 
Instance details

Defined in TPTP.AS

Methods

compare :: THF_atom -> THF_atom -> Ordering

(<) :: THF_atom -> THF_atom -> Bool

(<=) :: THF_atom -> THF_atom -> Bool

(>) :: THF_atom -> THF_atom -> Bool

(>=) :: THF_atom -> THF_atom -> Bool

max :: THF_atom -> THF_atom -> THF_atom

min :: THF_atom -> THF_atom -> THF_atom

Show THF_atom Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_atom -> ShowS

show :: THF_atom -> String

showList :: [THF_atom] -> ShowS

Generic THF_atom 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_atom :: Type -> Type

Methods

from :: THF_atom -> Rep THF_atom x

to :: Rep THF_atom x -> THF_atom

GetRange THF_atom Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_atom 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_atom

parseJSONList :: Value -> Parser [THF_atom]

ToJSON THF_atom 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_atom -> Value

toEncoding :: THF_atom -> Encoding

toJSONList :: [THF_atom] -> Value

toEncodingList :: [THF_atom] -> Encoding

ShATermConvertible THF_atom 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_atom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_atom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_atom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_atom])

Pretty THF_atom Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_atom 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_atom = D1 ('MetaData "THF_atom" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "THF_atom_function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_function)) :+: C1 ('MetaCons "THF_atom_variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Variable))) :+: (C1 ('MetaCons "THF_atom_defined" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Defined_term)) :+: C1 ('MetaCons "THF_atom_conn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_conn_term))))

data THF_function Source #

Instances

Instances details
Eq THF_function Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_function -> THF_function -> Bool

(/=) :: THF_function -> THF_function -> Bool

Data THF_function Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_function -> Constr

dataTypeOf :: THF_function -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_function -> THF_function

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

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

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

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

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

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

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

Ord THF_function Source # 
Instance details

Defined in TPTP.AS

Show THF_function Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_function -> ShowS

show :: THF_function -> String

showList :: [THF_function] -> ShowS

Generic THF_function 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_function :: Type -> Type

GetRange THF_function Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_function 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_function

parseJSONList :: Value -> Parser [THF_function]

ToJSON THF_function 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_function -> Value

toEncoding :: THF_function -> Encoding

toJSONList :: [THF_function] -> Value

toEncodingList :: [THF_function] -> Encoding

ShATermConvertible THF_function 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_function -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_function] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_function)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_function])

Pretty THF_function Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_function 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_function = D1 ('MetaData "THF_function" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "THFF_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Atom)) :+: C1 ('MetaCons "THFF_functor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPTP_functor) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_arguments))) :+: (C1 ('MetaCons "THFF_defined" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Defined_functor) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_arguments)) :+: C1 ('MetaCons "THFF_system" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 System_functor) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_arguments))))

data THF_conn_term Source #

Instances

Instances details
Eq THF_conn_term Source # 
Instance details

Defined in TPTP.AS

Data THF_conn_term Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_conn_term -> Constr

dataTypeOf :: THF_conn_term -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_conn_term -> THF_conn_term

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

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

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

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

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

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

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

Ord THF_conn_term Source # 
Instance details

Defined in TPTP.AS

Show THF_conn_term Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_conn_term -> ShowS

show :: THF_conn_term -> String

showList :: [THF_conn_term] -> ShowS

Generic THF_conn_term 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_conn_term :: Type -> Type

GetRange THF_conn_term Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_conn_term 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_conn_term

parseJSONList :: Value -> Parser [THF_conn_term]

ToJSON THF_conn_term 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_conn_term -> Value

toEncoding :: THF_conn_term -> Encoding

toJSONList :: [THF_conn_term] -> Value

toEncodingList :: [THF_conn_term] -> Encoding

ShATermConvertible THF_conn_term 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_conn_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_conn_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conn_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_conn_term])

Pretty THF_conn_term Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_conn_term 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_conn_term = D1 ('MetaData "THF_conn_term" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFC_pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_pair_connective)) :+: (C1 ('MetaCons "THFC_assoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assoc_connective)) :+: C1 ('MetaCons "THFC_unary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unary_connective))))

data THF_conditional Source #

Instances

Instances details
Eq THF_conditional Source # 
Instance details

Defined in TPTP.AS

Data THF_conditional Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_conditional -> Constr

dataTypeOf :: THF_conditional -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_conditional -> THF_conditional

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

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

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

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

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

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

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

Ord THF_conditional Source # 
Instance details

Defined in TPTP.AS

Show THF_conditional Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_conditional -> ShowS

show :: THF_conditional -> String

showList :: [THF_conditional] -> ShowS

Generic THF_conditional 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_conditional :: Type -> Type

GetRange THF_conditional Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_conditional 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_conditional

parseJSONList :: Value -> Parser [THF_conditional]

ToJSON THF_conditional 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_conditional -> Value

toEncoding :: THF_conditional -> Encoding

toJSONList :: [THF_conditional] -> Value

toEncodingList :: [THF_conditional] -> Encoding

ShATermConvertible THF_conditional 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_conditional -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_conditional] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conditional)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_conditional])

Pretty THF_conditional Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_conditional 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_conditional = D1 ('MetaData "THF_conditional" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_conditional" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula))))

data THF_let Source #

Instances

Instances details
Eq THF_let Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_let -> THF_let -> Bool

(/=) :: THF_let -> THF_let -> Bool

Data THF_let Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let -> Constr

dataTypeOf :: THF_let -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let -> THF_let

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

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

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

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

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

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

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

Ord THF_let Source # 
Instance details

Defined in TPTP.AS

Methods

compare :: THF_let -> THF_let -> Ordering

(<) :: THF_let -> THF_let -> Bool

(<=) :: THF_let -> THF_let -> Bool

(>) :: THF_let -> THF_let -> Bool

(>=) :: THF_let -> THF_let -> Bool

max :: THF_let -> THF_let -> THF_let

min :: THF_let -> THF_let -> THF_let

Show THF_let Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_let -> ShowS

show :: THF_let -> String

showList :: [THF_let] -> ShowS

Generic THF_let 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let :: Type -> Type

Methods

from :: THF_let -> Rep THF_let x

to :: Rep THF_let x -> THF_let

GetRange THF_let Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let

parseJSONList :: Value -> Parser [THF_let]

ToJSON THF_let 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_let -> Value

toEncoding :: THF_let -> Encoding

toJSONList :: [THF_let] -> Value

toEncodingList :: [THF_let] -> Encoding

ShATermConvertible THF_let 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let])

Pretty THF_let Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let = D1 ('MetaData "THF_let" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_defns) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_formula)))

data THF_let_defns Source #

Instances

Instances details
Eq THF_let_defns Source # 
Instance details

Defined in TPTP.AS

Data THF_let_defns Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let_defns -> Constr

dataTypeOf :: THF_let_defns -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let_defns -> THF_let_defns

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

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

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

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

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

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

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

Ord THF_let_defns Source # 
Instance details

Defined in TPTP.AS

Show THF_let_defns Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_let_defns -> ShowS

show :: THF_let_defns -> String

showList :: [THF_let_defns] -> ShowS

Generic THF_let_defns 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let_defns :: Type -> Type

GetRange THF_let_defns Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let_defns 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let_defns

parseJSONList :: Value -> Parser [THF_let_defns]

ToJSON THF_let_defns 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_let_defns -> Value

toEncoding :: THF_let_defns -> Encoding

toJSONList :: [THF_let_defns] -> Value

toEncodingList :: [THF_let_defns] -> Encoding

ShATermConvertible THF_let_defns 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let_defns -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defns] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defns)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defns])

Pretty THF_let_defns Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let_defns 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let_defns = D1 ('MetaData "THF_let_defns" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFLD_single" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_defn)) :+: C1 ('MetaCons "THFLD_many" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_defn_list)))

data THF_let_defn Source #

Instances

Instances details
Eq THF_let_defn Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_let_defn -> THF_let_defn -> Bool

(/=) :: THF_let_defn -> THF_let_defn -> Bool

Data THF_let_defn Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let_defn -> Constr

dataTypeOf :: THF_let_defn -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let_defn -> THF_let_defn

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

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

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

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

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

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

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

Ord THF_let_defn Source # 
Instance details

Defined in TPTP.AS

Show THF_let_defn Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_let_defn -> ShowS

show :: THF_let_defn -> String

showList :: [THF_let_defn] -> ShowS

Generic THF_let_defn 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let_defn :: Type -> Type

GetRange THF_let_defn Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let_defn

parseJSONList :: Value -> Parser [THF_let_defn]

ToJSON THF_let_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_let_defn -> Value

toEncoding :: THF_let_defn -> Encoding

toJSONList :: [THF_let_defn] -> Value

toEncodingList :: [THF_let_defn] -> Encoding

ShATermConvertible THF_let_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defn])

Pretty THF_let_defn Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let_defn 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let_defn = D1 ('MetaData "THF_let_defn" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFLD_quantified" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_quantified_defn)) :+: C1 ('MetaCons "THFLD_plain" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_plain_defn)))

data THF_let_quantified_defn Source #

Instances

Instances details
Eq THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.AS

Data THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let_quantified_defn -> Constr

dataTypeOf :: THF_let_quantified_defn -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let_quantified_defn -> THF_let_quantified_defn

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

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

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

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

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

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

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

Ord THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.AS

Show THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.AS

Generic THF_let_quantified_defn 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let_quantified_defn :: Type -> Type

GetRange THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let_quantified_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let_quantified_defn

parseJSONList :: Value -> Parser [THF_let_quantified_defn]

ToJSON THF_let_quantified_defn 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_let_quantified_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let_quantified_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_quantified_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_quantified_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_quantified_defn])

Pretty THF_let_quantified_defn Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let_quantified_defn 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let_quantified_defn = D1 ('MetaData "THF_let_quantified_defn" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_let_quantified_defn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_quantification) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_plain_defn)))

data THF_let_plain_defn Source #

Instances

Instances details
Eq THF_let_plain_defn Source # 
Instance details

Defined in TPTP.AS

Data THF_let_plain_defn Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let_plain_defn -> Constr

dataTypeOf :: THF_let_plain_defn -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let_plain_defn -> THF_let_plain_defn

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

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

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

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

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

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

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

Ord THF_let_plain_defn Source # 
Instance details

Defined in TPTP.AS

Show THF_let_plain_defn Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_let_plain_defn -> ShowS

show :: THF_let_plain_defn -> String

showList :: [THF_let_plain_defn] -> ShowS

Generic THF_let_plain_defn 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let_plain_defn :: Type -> Type

GetRange THF_let_plain_defn Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let_plain_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let_plain_defn

parseJSONList :: Value -> Parser [THF_let_plain_defn]

ToJSON THF_let_plain_defn 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_let_plain_defn 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let_plain_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_plain_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_plain_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_plain_defn])

Pretty THF_let_plain_defn Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let_plain_defn 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let_plain_defn = D1 ('MetaData "THF_let_plain_defn" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_let_plain_defn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_let_defn_LHS) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_formula)))

data THF_let_defn_LHS Source #

Instances

Instances details
Eq THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.AS

Data THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_let_defn_LHS -> Constr

dataTypeOf :: THF_let_defn_LHS -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_let_defn_LHS -> THF_let_defn_LHS

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

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

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

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

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

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

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

Ord THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.AS

Show THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_let_defn_LHS -> ShowS

show :: THF_let_defn_LHS -> String

showList :: [THF_let_defn_LHS] -> ShowS

Generic THF_let_defn_LHS 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_let_defn_LHS :: Type -> Type

GetRange THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_let_defn_LHS 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_let_defn_LHS

parseJSONList :: Value -> Parser [THF_let_defn_LHS]

ToJSON THF_let_defn_LHS 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_let_defn_LHS 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_let_defn_LHS -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defn_LHS] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn_LHS)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defn_LHS])

Pretty THF_let_defn_LHS Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_let_defn_LHS 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_let_defn_LHS = D1 ('MetaData "THF_let_defn_LHS" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFLDL_constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant)) :+: (C1 ('MetaCons "THFLDL_functor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPTP_functor) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FOF_arguments)) :+: C1 ('MetaCons "THFLDL_tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_tuple))))

data THF_type_formula Source #

Instances

Instances details
Eq THF_type_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_type_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_type_formula -> Constr

dataTypeOf :: THF_type_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_type_formula -> THF_type_formula

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

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

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

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

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

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

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

Ord THF_type_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_type_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_type_formula -> ShowS

show :: THF_type_formula -> String

showList :: [THF_type_formula] -> ShowS

Generic THF_type_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_type_formula :: Type -> Type

GetRange THF_type_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_type_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_type_formula

parseJSONList :: Value -> Parser [THF_type_formula]

ToJSON THF_type_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_type_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_type_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_type_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_type_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_type_formula])

Pretty THF_type_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_type_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_type_formula = D1 ('MetaData "THF_type_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFTF_typeable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_typeable_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_top_level_type)) :+: C1 ('MetaCons "THFTF_constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_top_level_type)))

data THF_typeable_formula Source #

Instances

Instances details
Eq THF_typeable_formula Source # 
Instance details

Defined in TPTP.AS

Data THF_typeable_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_typeable_formula -> Constr

dataTypeOf :: THF_typeable_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_typeable_formula -> THF_typeable_formula

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

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

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

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

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

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

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

Ord THF_typeable_formula Source # 
Instance details

Defined in TPTP.AS

Show THF_typeable_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_typeable_formula -> ShowS

show :: THF_typeable_formula -> String

showList :: [THF_typeable_formula] -> ShowS

Generic THF_typeable_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_typeable_formula :: Type -> Type

GetRange THF_typeable_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_typeable_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_typeable_formula

parseJSONList :: Value -> Parser [THF_typeable_formula]

ToJSON THF_typeable_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_typeable_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_typeable_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_typeable_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typeable_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_typeable_formula])

Pretty THF_typeable_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_typeable_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_typeable_formula = D1 ('MetaData "THF_typeable_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFTF_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_atom)) :+: C1 ('MetaCons "THFTF_logic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_logic_formula)))

data THF_subtype Source #

Instances

Instances details
Eq THF_subtype Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_subtype -> THF_subtype -> Bool

(/=) :: THF_subtype -> THF_subtype -> Bool

Data THF_subtype Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_subtype -> Constr

dataTypeOf :: THF_subtype -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_subtype -> THF_subtype

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

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

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

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

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

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

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

Ord THF_subtype Source # 
Instance details

Defined in TPTP.AS

Show THF_subtype Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_subtype -> ShowS

show :: THF_subtype -> String

showList :: [THF_subtype] -> ShowS

Generic THF_subtype 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_subtype :: Type -> Type

Methods

from :: THF_subtype -> Rep THF_subtype x

to :: Rep THF_subtype x -> THF_subtype

GetRange THF_subtype Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_subtype 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_subtype

parseJSONList :: Value -> Parser [THF_subtype]

ToJSON THF_subtype 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_subtype -> Value

toEncoding :: THF_subtype -> Encoding

toJSONList :: [THF_subtype] -> Value

toEncodingList :: [THF_subtype] -> Encoding

ShATermConvertible THF_subtype 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_subtype -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_subtype] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_subtype)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_subtype])

Pretty THF_subtype Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_subtype 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_subtype = D1 ('MetaData "THF_subtype" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THF_subtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_atom) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_atom)))

data THF_top_level_type Source #

Instances

Instances details
Eq THF_top_level_type Source # 
Instance details

Defined in TPTP.AS

Data THF_top_level_type Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_top_level_type -> Constr

dataTypeOf :: THF_top_level_type -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_top_level_type -> THF_top_level_type

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

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

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

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

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

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

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

Ord THF_top_level_type Source # 
Instance details

Defined in TPTP.AS

Show THF_top_level_type Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_top_level_type -> ShowS

show :: THF_top_level_type -> String

showList :: [THF_top_level_type] -> ShowS

Generic THF_top_level_type 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_top_level_type :: Type -> Type

GetRange THF_top_level_type Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_top_level_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_top_level_type

parseJSONList :: Value -> Parser [THF_top_level_type]

ToJSON THF_top_level_type 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_top_level_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_top_level_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_top_level_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_top_level_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_top_level_type])

Pretty THF_top_level_type Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_top_level_type 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_top_level_type = D1 ('MetaData "THF_top_level_type" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFTLT_unitary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_type)) :+: C1 ('MetaCons "THFTLT_mapping" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_mapping_type)))

data THF_unitary_type Source #

Instances

Instances details
Eq THF_unitary_type Source # 
Instance details

Defined in TPTP.AS

Data THF_unitary_type Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_unitary_type -> Constr

dataTypeOf :: THF_unitary_type -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_unitary_type -> THF_unitary_type

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

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

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

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

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

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

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

Ord THF_unitary_type Source # 
Instance details

Defined in TPTP.AS

Show THF_unitary_type Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_unitary_type -> ShowS

show :: THF_unitary_type -> String

showList :: [THF_unitary_type] -> ShowS

Generic THF_unitary_type 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_unitary_type :: Type -> Type

GetRange THF_unitary_type Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_unitary_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_unitary_type

parseJSONList :: Value -> Parser [THF_unitary_type]

ToJSON THF_unitary_type 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible THF_unitary_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_unitary_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unitary_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unitary_type])

Pretty THF_unitary_type Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_unitary_type 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_unitary_type = D1 ('MetaData "THF_unitary_type" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFUT_unitary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula)) :+: C1 ('MetaCons "THFUT_binary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_binary_type)))

data THF_binary_type Source #

Instances

Instances details
Eq THF_binary_type Source # 
Instance details

Defined in TPTP.AS

Data THF_binary_type Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_binary_type -> Constr

dataTypeOf :: THF_binary_type -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_binary_type -> THF_binary_type

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

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

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

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

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

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

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

Ord THF_binary_type Source # 
Instance details

Defined in TPTP.AS

Show THF_binary_type Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_binary_type -> ShowS

show :: THF_binary_type -> String

showList :: [THF_binary_type] -> ShowS

Generic THF_binary_type 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_binary_type :: Type -> Type

GetRange THF_binary_type Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_binary_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_binary_type

parseJSONList :: Value -> Parser [THF_binary_type]

ToJSON THF_binary_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_binary_type -> Value

toEncoding :: THF_binary_type -> Encoding

toJSONList :: [THF_binary_type] -> Value

toEncodingList :: [THF_binary_type] -> Encoding

ShATermConvertible THF_binary_type 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_binary_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_type])

Pretty THF_binary_type Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_binary_type 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_binary_type = D1 ('MetaData "THF_binary_type" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFBT_mapping" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_mapping_type)) :+: (C1 ('MetaCons "THFBT_xprod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_xprod_type)) :+: C1 ('MetaCons "THFBT_union" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_union_type))))

data THF_sequent Source #

Instances

Instances details
Eq THF_sequent Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_sequent -> THF_sequent -> Bool

(/=) :: THF_sequent -> THF_sequent -> Bool

Data THF_sequent Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_sequent -> Constr

dataTypeOf :: THF_sequent -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_sequent -> THF_sequent

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

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

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

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

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

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

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

Ord THF_sequent Source # 
Instance details

Defined in TPTP.AS

Show THF_sequent Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_sequent -> ShowS

show :: THF_sequent -> String

showList :: [THF_sequent] -> ShowS

Generic THF_sequent 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_sequent :: Type -> Type

Methods

from :: THF_sequent -> Rep THF_sequent x

to :: Rep THF_sequent x -> THF_sequent

GetRange THF_sequent Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_sequent 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_sequent

parseJSONList :: Value -> Parser [THF_sequent]

ToJSON THF_sequent 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_sequent -> Value

toEncoding :: THF_sequent -> Encoding

toJSONList :: [THF_sequent] -> Value

toEncodingList :: [THF_sequent] -> Encoding

ShATermConvertible THF_sequent 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_sequent -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_sequent] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_sequent)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_sequent])

Pretty THF_sequent Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_sequent 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_sequent = D1 ('MetaData "THF_sequent" "TPTP.AS" "main" 'False) (C1 ('MetaCons "THFS_plain" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_tuple) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_tuple)) :+: C1 ('MetaCons "THFS_parens" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_sequent)))

newtype THF_tuple Source #

Instances

Instances details
Eq THF_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: THF_tuple -> THF_tuple -> Bool

(/=) :: THF_tuple -> THF_tuple -> Bool

Data THF_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: THF_tuple -> Constr

dataTypeOf :: THF_tuple -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> THF_tuple -> THF_tuple

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

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

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

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

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

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

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

Ord THF_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

compare :: THF_tuple -> THF_tuple -> Ordering

(<) :: THF_tuple -> THF_tuple -> Bool

(<=) :: THF_tuple -> THF_tuple -> Bool

(>) :: THF_tuple -> THF_tuple -> Bool

(>=) :: THF_tuple -> THF_tuple -> Bool

max :: THF_tuple -> THF_tuple -> THF_tuple

min :: THF_tuple -> THF_tuple -> THF_tuple

Show THF_tuple Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> THF_tuple -> ShowS

show :: THF_tuple -> String

showList :: [THF_tuple] -> ShowS

Generic THF_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep THF_tuple :: Type -> Type

Methods

from :: THF_tuple -> Rep THF_tuple x

to :: Rep THF_tuple x -> THF_tuple

GetRange THF_tuple Source # 
Instance details

Defined in TPTP.AS

FromJSON THF_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser THF_tuple

parseJSONList :: Value -> Parser [THF_tuple]

ToJSON THF_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: THF_tuple -> Value

toEncoding :: THF_tuple -> Encoding

toJSONList :: [THF_tuple] -> Value

toEncodingList :: [THF_tuple] -> Encoding

ShATermConvertible THF_tuple 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> THF_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_tuple])

Pretty THF_tuple Source # 
Instance details

Defined in TPTP.Pretty

type Rep THF_tuple 
Instance details

Defined in TPTP.ATC_TPTP

type Rep THF_tuple = D1 ('MetaData "THF_tuple" "TPTP.AS" "main" 'True) (C1 ('MetaCons "THF_tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_formula_list)))

data TFX_formula Source #

Instances

Instances details
Eq TFX_formula Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: TFX_formula -> TFX_formula -> Bool

(/=) :: TFX_formula -> TFX_formula -> Bool

Data TFX_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFX_formula -> Constr

dataTypeOf :: TFX_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFX_formula -> TFX_formula

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

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

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

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

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

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

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

Ord TFX_formula Source # 
Instance details

Defined in TPTP.AS

Show TFX_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFX_formula -> ShowS

show :: TFX_formula -> String

showList :: [TFX_formula] -> ShowS

Generic TFX_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFX_formula :: Type -> Type

Methods

from :: TFX_formula -> Rep TFX_formula x

to :: Rep TFX_formula x -> TFX_formula

GetRange TFX_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON TFX_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFX_formula

parseJSONList :: Value -> Parser [TFX_formula]

ToJSON TFX_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TFX_formula -> Value

toEncoding :: TFX_formula -> Encoding

toJSONList :: [TFX_formula] -> Value

toEncodingList :: [TFX_formula] -> Encoding

ShATermConvertible TFX_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFX_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_formula])

Pretty TFX_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFX_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFX_formula = D1 ('MetaData "TFX_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFXF_logic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFX_logic_formula)) :+: C1 ('MetaCons "TFXF_sequent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_sequent)))

data TFX_logic_formula Source #

Instances

Instances details
Eq TFX_logic_formula Source # 
Instance details

Defined in TPTP.AS

Data TFX_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFX_logic_formula -> Constr

dataTypeOf :: TFX_logic_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFX_logic_formula -> TFX_logic_formula

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

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

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

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

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

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

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

Ord TFX_logic_formula Source # 
Instance details

Defined in TPTP.AS

Show TFX_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFX_logic_formula -> ShowS

show :: TFX_logic_formula -> String

showList :: [TFX_logic_formula] -> ShowS

Generic TFX_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFX_logic_formula :: Type -> Type

GetRange TFX_logic_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON TFX_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFX_logic_formula

parseJSONList :: Value -> Parser [TFX_logic_formula]

ToJSON TFX_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible TFX_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFX_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_logic_formula])

Pretty TFX_logic_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFX_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFX_logic_formula = D1 ('MetaData "TFX_logic_formula" "TPTP.AS" "main" 'False) ((C1 ('MetaCons "TFXLF_binary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_binary_formula)) :+: C1 ('MetaCons "TFXLF_unitary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THF_unitary_formula))) :+: (C1 ('MetaCons "TFXLF_typed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_typed_atom)) :+: C1 ('MetaCons "TFXLF_subtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_subtype))))

data TFF_formula Source #

Instances

Instances details
Eq TFF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

(==) :: TFF_formula -> TFF_formula -> Bool

(/=) :: TFF_formula -> TFF_formula -> Bool

Data TFF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFF_formula -> Constr

dataTypeOf :: TFF_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFF_formula -> TFF_formula

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

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

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

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

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

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

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

Ord TFF_formula Source # 
Instance details

Defined in TPTP.AS

Show TFF_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFF_formula -> ShowS

show :: TFF_formula -> String

showList :: [TFF_formula] -> ShowS

Generic TFF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFF_formula :: Type -> Type

Methods

from :: TFF_formula -> Rep TFF_formula x

to :: Rep TFF_formula x -> TFF_formula

GetRange TFF_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON TFF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFF_formula

parseJSONList :: Value -> Parser [TFF_formula]

ToJSON TFF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toJSON :: TFF_formula -> Value

toEncoding :: TFF_formula -> Encoding

toJSONList :: [TFF_formula] -> Value

toEncodingList :: [TFF_formula] -> Encoding

ShATermConvertible TFF_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_formula])

Pretty TFF_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFF_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFF_formula = D1 ('MetaData "TFF_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFFF_logic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_logic_formula)) :+: (C1 ('MetaCons "TFFF_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_typed_atom)) :+: C1 ('MetaCons "TFFF_sequent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_sequent))))

data TFF_logic_formula Source #

Instances

Instances details
Eq TFF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Data TFF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFF_logic_formula -> Constr

dataTypeOf :: TFF_logic_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFF_logic_formula -> TFF_logic_formula

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

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

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

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

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

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

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

Ord TFF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Show TFF_logic_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFF_logic_formula -> ShowS

show :: TFF_logic_formula -> String

showList :: [TFF_logic_formula] -> ShowS

Generic TFF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFF_logic_formula :: Type -> Type

GetRange TFF_logic_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON TFF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFF_logic_formula

parseJSONList :: Value -> Parser [TFF_logic_formula]

ToJSON TFF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible TFF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_logic_formula])

Pretty TFF_logic_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFF_logic_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFF_logic_formula = D1 ('MetaData "TFF_logic_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFFLF_binary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_binary_formula)) :+: (C1 ('MetaCons "TFFLF_unitary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_unitary_formula)) :+: C1 ('MetaCons "TFFLF_subtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_subtype))))

data TFF_binary_formula Source #

Instances

Instances details
Eq TFF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Data TFF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFF_binary_formula -> Constr

dataTypeOf :: TFF_binary_formula -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFF_binary_formula -> TFF_binary_formula

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

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

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

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

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

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

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

Ord TFF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Show TFF_binary_formula Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFF_binary_formula -> ShowS

show :: TFF_binary_formula -> String

showList :: [TFF_binary_formula] -> ShowS

Generic TFF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFF_binary_formula :: Type -> Type

GetRange TFF_binary_formula Source # 
Instance details

Defined in TPTP.AS

FromJSON TFF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFF_binary_formula

parseJSONList :: Value -> Parser [TFF_binary_formula]

ToJSON TFF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible TFF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFF_binary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_binary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_binary_formula])

Pretty TFF_binary_formula Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFF_binary_formula 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFF_binary_formula = D1 ('MetaData "TFF_binary_formula" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFFBF_nonassoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_binary_nonassoc)) :+: C1 ('MetaCons "TFFBF_assoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_binary_assoc)))

data TFF_binary_nonassoc Source #

Instances

Instances details
Eq TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.AS

Data TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.AS

Methods

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

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

toConstr :: TFF_binary_nonassoc -> Constr

dataTypeOf :: TFF_binary_nonassoc -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> TFF_binary_nonassoc -> TFF_binary_nonassoc

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

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

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

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

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

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

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

Ord TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.AS

Show TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.AS

Methods

showsPrec :: Int -> TFF_binary_nonassoc -> ShowS

show :: TFF_binary_nonassoc -> String

showList :: [TFF_binary_nonassoc] -> ShowS

Generic TFF_binary_nonassoc 
Instance details

Defined in TPTP.ATC_TPTP

Associated Types

type Rep TFF_binary_nonassoc :: Type -> Type

GetRange TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.AS

FromJSON TFF_binary_nonassoc 
Instance details

Defined in TPTP.ATC_TPTP

Methods

parseJSON :: Value -> Parser TFF_binary_nonassoc

parseJSONList :: Value -> Parser [TFF_binary_nonassoc]

ToJSON TFF_binary_nonassoc 
Instance details

Defined in TPTP.ATC_TPTP

ShATermConvertible TFF_binary_nonassoc 
Instance details

Defined in TPTP.ATC_TPTP

Methods

toShATermAux :: ATermTable -> TFF_binary_nonassoc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_binary_nonassoc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_nonassoc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_binary_nonassoc])

Pretty TFF_binary_nonassoc Source # 
Instance details

Defined in TPTP.Pretty

type Rep TFF_binary_nonassoc 
Instance details

Defined in TPTP.ATC_TPTP

type Rep TFF_binary_nonassoc = D1 ('MetaData "TFF_binary_nonassoc" "TPTP.AS" "main" 'False) (C1 ('MetaCons "TFF_binary_nonassoc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Binary_connective) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_unitary_formula) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFF_unitary_formula))))

data TFF_binary_assoc Source #

Instances

Instances details