Copyright | (c) Eugen Kuksa University of Magdeburg 2017 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Eugen Kuksa <kuksa@iks.cs.ovgu.de> |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
TPTP.AS
Description
Definition of abstract syntax for TPTP taken from [1]
References
- 1
- G. Sutcliffe et al.: The TPTP language grammar in BNF.
http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html
Note: The implemented version is saved at TPTPDocumentsSyntaxBNF.html
Note: The names of the data types are aligned with the names of the grammar rules at this reference page (modulo case).
- 2
- C. Kaliszyk, G. Sutcliffe and F. Rabe: TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism https://kwarc.info/people/frabe/Research/KRS_thf1_16.pdf Note: for further information on TF0, TF1, TH0 and TH1
Documentation
newtype BASIC_SPEC Source #
Constructors
Basic_spec [Annoted TPTP] |
Instances
Constructors
TPTP [TPTP_input] |
Instances
Eq TPTP Source # | |
Data TPTP Source # | |
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 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 # | |
Show TPTP Source # | |
Generic TPTP | |
GetRange TPTP Source # | |
FromJSON TPTP | |
Defined in TPTP.ATC_TPTP | |
ToJSON TPTP | |
Defined in TPTP.ATC_TPTP Methods toEncoding :: TPTP -> Encoding toJSONList :: [TPTP] -> Value toEncodingList :: [TPTP] -> Encoding | |
ShATermConvertible TPTP | |
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 # | |
type Rep TPTP | |
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 #
Constructors
Annotated_formula Annotated_formula | |
TPTP_include Include | |
TPTP_comment Comment | |
TPTP_defined_comment DefinedComment | |
TPTP_system_comment SystemComment |
Instances
Eq TPTP_input Source # | |
Defined in TPTP.AS | |
Data TPTP_input Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TPTP_input -> TPTP_input -> Ordering (<) :: TPTP_input -> TPTP_input -> Bool (<=) :: TPTP_input -> TPTP_input -> Bool (>) :: TPTP_input -> TPTP_input -> Bool (>=) :: TPTP_input -> TPTP_input -> Bool max :: TPTP_input -> TPTP_input -> TPTP_input min :: TPTP_input -> TPTP_input -> TPTP_input | |
Show TPTP_input Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TPTP_input -> ShowS show :: TPTP_input -> String showList :: [TPTP_input] -> ShowS | |
Generic TPTP_input | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TPTP_input :: Type -> Type | |
GetRange TPTP_input Source # | |
FromJSON TPTP_input | |
Defined in TPTP.ATC_TPTP | |
ToJSON TPTP_input | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TPTP_input | |
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))))) |
Constructors
Comment_line Token | |
Comment_block Token |
Instances
Eq Comment Source # | |
Data Comment Source # | |
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 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 # | |
Show Comment Source # | |
Generic Comment | |
GetRange Comment Source # | |
FromJSON Comment | |
Defined in TPTP.ATC_TPTP | |
ToJSON Comment | |
Defined in TPTP.ATC_TPTP Methods toEncoding :: Comment -> Encoding toJSONList :: [Comment] -> Value toEncodingList :: [Comment] -> Encoding | |
ShATermConvertible Comment | |
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 # | |
type Rep Comment | |
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 #
Constructors
Defined_comment_line Token | |
Defined_comment_block Token |
Instances
Eq DefinedComment Source # | |
Defined in TPTP.AS Methods (==) :: DefinedComment -> DefinedComment -> Bool (/=) :: DefinedComment -> DefinedComment -> Bool | |
Data DefinedComment Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: DefinedComment -> DefinedComment -> Ordering (<) :: DefinedComment -> DefinedComment -> Bool (<=) :: DefinedComment -> DefinedComment -> Bool (>) :: DefinedComment -> DefinedComment -> Bool (>=) :: DefinedComment -> DefinedComment -> Bool max :: DefinedComment -> DefinedComment -> DefinedComment min :: DefinedComment -> DefinedComment -> DefinedComment | |
Show DefinedComment Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> DefinedComment -> ShowS show :: DefinedComment -> String showList :: [DefinedComment] -> ShowS | |
Generic DefinedComment | |
Defined in TPTP.ATC_TPTP Associated Types type Rep DefinedComment :: Type -> Type | |
GetRange DefinedComment Source # | |
FromJSON DefinedComment | |
Defined in TPTP.ATC_TPTP | |
ToJSON DefinedComment | |
Defined in TPTP.ATC_TPTP Methods toJSON :: DefinedComment -> Value toEncoding :: DefinedComment -> Encoding toJSONList :: [DefinedComment] -> Value toEncodingList :: [DefinedComment] -> Encoding | |
ShATermConvertible DefinedComment | |
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 # | |
Defined in TPTP.Pretty | |
type Rep DefinedComment | |
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 #
Constructors
System_comment_line Token | |
System_comment_block Token |
Instances
Eq SystemComment Source # | |
Defined in TPTP.AS | |
Data SystemComment Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: SystemComment -> SystemComment -> Ordering (<) :: SystemComment -> SystemComment -> Bool (<=) :: SystemComment -> SystemComment -> Bool (>) :: SystemComment -> SystemComment -> Bool (>=) :: SystemComment -> SystemComment -> Bool max :: SystemComment -> SystemComment -> SystemComment min :: SystemComment -> SystemComment -> SystemComment | |
Show SystemComment Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> SystemComment -> ShowS show :: SystemComment -> String showList :: [SystemComment] -> ShowS | |
Generic SystemComment | |
Defined in TPTP.ATC_TPTP Associated Types type Rep SystemComment :: Type -> Type | |
GetRange SystemComment Source # | |
FromJSON SystemComment | |
Defined in TPTP.ATC_TPTP | |
ToJSON SystemComment | |
Defined in TPTP.ATC_TPTP Methods toJSON :: SystemComment -> Value toEncoding :: SystemComment -> Encoding toJSONList :: [SystemComment] -> Value toEncodingList :: [SystemComment] -> Encoding | |
ShATermConvertible SystemComment | |
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 # | |
Defined in TPTP.Pretty | |
type Rep SystemComment | |
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 #
Constructors
Instances
data TPI_annotated Source #
Constructors
TPI_annotated Name Formula_role TPI_formula Annotations |
Instances
Eq TPI_annotated Source # | |
Defined in TPTP.AS | |
Data TPI_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TPI_annotated -> TPI_annotated -> Ordering (<) :: TPI_annotated -> TPI_annotated -> Bool (<=) :: TPI_annotated -> TPI_annotated -> Bool (>) :: TPI_annotated -> TPI_annotated -> Bool (>=) :: TPI_annotated -> TPI_annotated -> Bool max :: TPI_annotated -> TPI_annotated -> TPI_annotated min :: TPI_annotated -> TPI_annotated -> TPI_annotated | |
Show TPI_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TPI_annotated -> ShowS show :: TPI_annotated -> String showList :: [TPI_annotated] -> ShowS | |
Generic TPI_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TPI_annotated :: Type -> Type | |
GetRange TPI_annotated Source # | |
FromJSON TPI_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON TPI_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TPI_annotated | |
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)))) |
type TPI_formula = FOF_formula Source #
data THF_annotated Source #
Constructors
THF_annotated Name Formula_role THF_formula Annotations |
Instances
Eq THF_annotated Source # | |
Defined in TPTP.AS | |
Data THF_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_annotated -> THF_annotated -> Ordering (<) :: THF_annotated -> THF_annotated -> Bool (<=) :: THF_annotated -> THF_annotated -> Bool (>) :: THF_annotated -> THF_annotated -> Bool (>=) :: THF_annotated -> THF_annotated -> Bool max :: THF_annotated -> THF_annotated -> THF_annotated min :: THF_annotated -> THF_annotated -> THF_annotated | |
Show THF_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_annotated -> ShowS show :: THF_annotated -> String showList :: [THF_annotated] -> ShowS | |
Generic THF_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_annotated :: Type -> Type | |
GetRange THF_annotated Source # | |
FromJSON THF_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_annotated | |
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 #
Constructors
TFX_annotated Name Formula_role TFX_formula Annotations |
Instances
Eq TFX_annotated Source # | |
Defined in TPTP.AS | |
Data TFX_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFX_annotated -> TFX_annotated -> Ordering (<) :: TFX_annotated -> TFX_annotated -> Bool (<=) :: TFX_annotated -> TFX_annotated -> Bool (>) :: TFX_annotated -> TFX_annotated -> Bool (>=) :: TFX_annotated -> TFX_annotated -> Bool max :: TFX_annotated -> TFX_annotated -> TFX_annotated min :: TFX_annotated -> TFX_annotated -> TFX_annotated | |
Show TFX_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TFX_annotated -> ShowS show :: TFX_annotated -> String showList :: [TFX_annotated] -> ShowS | |
Generic TFX_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFX_annotated :: Type -> Type | |
GetRange TFX_annotated Source # | |
FromJSON TFX_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON TFX_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFX_annotated | |
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 #
Constructors
TFF_annotated Name Formula_role TFF_formula Annotations |
Instances
Eq TFF_annotated Source # | |
Defined in TPTP.AS | |
Data TFF_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFF_annotated -> TFF_annotated -> Ordering (<) :: TFF_annotated -> TFF_annotated -> Bool (<=) :: TFF_annotated -> TFF_annotated -> Bool (>) :: TFF_annotated -> TFF_annotated -> Bool (>=) :: TFF_annotated -> TFF_annotated -> Bool max :: TFF_annotated -> TFF_annotated -> TFF_annotated min :: TFF_annotated -> TFF_annotated -> TFF_annotated | |
Show TFF_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TFF_annotated -> ShowS show :: TFF_annotated -> String showList :: [TFF_annotated] -> ShowS | |
Generic TFF_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFF_annotated :: Type -> Type | |
GetRange TFF_annotated Source # | |
FromJSON TFF_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON TFF_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFF_annotated | |
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 #
Constructors
TCF_annotated Name Formula_role TCF_formula Annotations |
Instances
Eq TCF_annotated Source # | |
Defined in TPTP.AS | |
Data TCF_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TCF_annotated -> TCF_annotated -> Ordering (<) :: TCF_annotated -> TCF_annotated -> Bool (<=) :: TCF_annotated -> TCF_annotated -> Bool (>) :: TCF_annotated -> TCF_annotated -> Bool (>=) :: TCF_annotated -> TCF_annotated -> Bool max :: TCF_annotated -> TCF_annotated -> TCF_annotated min :: TCF_annotated -> TCF_annotated -> TCF_annotated | |
Show TCF_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TCF_annotated -> ShowS show :: TCF_annotated -> String showList :: [TCF_annotated] -> ShowS | |
Generic TCF_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TCF_annotated :: Type -> Type | |
GetRange TCF_annotated Source # | |
FromJSON TCF_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON TCF_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TCF_annotated | |
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 #
Constructors
FOF_annotated Name Formula_role FOF_formula Annotations |
Instances
Eq FOF_annotated Source # | |
Defined in TPTP.AS | |
Data FOF_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: FOF_annotated -> FOF_annotated -> Ordering (<) :: FOF_annotated -> FOF_annotated -> Bool (<=) :: FOF_annotated -> FOF_annotated -> Bool (>) :: FOF_annotated -> FOF_annotated -> Bool (>=) :: FOF_annotated -> FOF_annotated -> Bool max :: FOF_annotated -> FOF_annotated -> FOF_annotated min :: FOF_annotated -> FOF_annotated -> FOF_annotated | |
Show FOF_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> FOF_annotated -> ShowS show :: FOF_annotated -> String showList :: [FOF_annotated] -> ShowS | |
Generic FOF_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep FOF_annotated :: Type -> Type | |
GetRange FOF_annotated Source # | |
FromJSON FOF_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON FOF_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep FOF_annotated | |
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 #
Constructors
CNF_annotated Name Formula_role CNF_formula Annotations |
Instances
Eq CNF_annotated Source # | |
Defined in TPTP.AS | |
Data CNF_annotated Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: CNF_annotated -> CNF_annotated -> Ordering (<) :: CNF_annotated -> CNF_annotated -> Bool (<=) :: CNF_annotated -> CNF_annotated -> Bool (>) :: CNF_annotated -> CNF_annotated -> Bool (>=) :: CNF_annotated -> CNF_annotated -> Bool max :: CNF_annotated -> CNF_annotated -> CNF_annotated min :: CNF_annotated -> CNF_annotated -> CNF_annotated | |
Show CNF_annotated Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> CNF_annotated -> ShowS show :: CNF_annotated -> String showList :: [CNF_annotated] -> ShowS | |
Generic CNF_annotated | |
Defined in TPTP.ATC_TPTP Associated Types type Rep CNF_annotated :: Type -> Type | |
GetRange CNF_annotated Source # | |
FromJSON CNF_annotated | |
Defined in TPTP.ATC_TPTP | |
ToJSON CNF_annotated | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep CNF_annotated | |
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)))) |
name :: Annotated_formula -> Name Source #
newtype Annotations Source #
Constructors
Annotations (Maybe (Source, Optional_info)) |
Instances
Eq Annotations Source # | |
Defined in TPTP.AS | |
Data Annotations Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: Annotations -> Annotations -> Ordering (<) :: Annotations -> Annotations -> Bool (<=) :: Annotations -> Annotations -> Bool (>) :: Annotations -> Annotations -> Bool (>=) :: Annotations -> Annotations -> Bool max :: Annotations -> Annotations -> Annotations min :: Annotations -> Annotations -> Annotations | |
Show Annotations Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> Annotations -> ShowS show :: Annotations -> String showList :: [Annotations] -> ShowS | |
Generic Annotations | |
Defined in TPTP.ATC_TPTP Associated Types type Rep Annotations :: Type -> Type | |
GetRange Annotations Source # | |
FromJSON Annotations | |
Defined in TPTP.ATC_TPTP | |
ToJSON Annotations | |
Defined in TPTP.ATC_TPTP Methods toJSON :: Annotations -> Value toEncoding :: Annotations -> Encoding toJSONList :: [Annotations] -> Value toEncodingList :: [Annotations] -> Encoding | |
ShATermConvertible Annotations | |
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 # | |
Defined in TPTP.Pretty | |
type Rep Annotations | |
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 #
Constructors
Axiom | |
Hypothesis | |
Definition | |
Assumption | |
Lemma | |
Theorem | |
Corollary | |
Conjecture | |
Negated_conjecture | |
Plain | |
Type | |
Fi_domain | |
Fi_functors | |
Fi_predicates | |
Unknown | |
Other_formula_role Token | For future updates. Should not be used. |
Instances
Eq Formula_role Source # | |
Defined in TPTP.AS | |
Data Formula_role Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: Formula_role -> Formula_role -> Ordering (<) :: Formula_role -> Formula_role -> Bool (<=) :: Formula_role -> Formula_role -> Bool (>) :: Formula_role -> Formula_role -> Bool (>=) :: Formula_role -> Formula_role -> Bool max :: Formula_role -> Formula_role -> Formula_role min :: Formula_role -> Formula_role -> Formula_role | |
Show Formula_role Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> Formula_role -> ShowS show :: Formula_role -> String showList :: [Formula_role] -> ShowS | |
Generic Formula_role | |
Defined in TPTP.ATC_TPTP Associated Types type Rep Formula_role :: Type -> Type | |
GetRange Formula_role Source # | |
FromJSON Formula_role | |
Defined in TPTP.ATC_TPTP | |
ToJSON Formula_role | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep Formula_role | |
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 #
Constructors
THFF_logic THF_logic_formula | |
THFF_sequent THF_sequent |
Instances
Eq THF_formula Source # | |
Defined in TPTP.AS | |
Data THF_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_formula -> THF_formula -> Ordering (<) :: THF_formula -> THF_formula -> Bool (<=) :: THF_formula -> THF_formula -> Bool (>) :: THF_formula -> THF_formula -> Bool (>=) :: THF_formula -> THF_formula -> Bool max :: THF_formula -> THF_formula -> THF_formula min :: THF_formula -> THF_formula -> THF_formula | |
Show THF_formula Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_formula -> ShowS show :: THF_formula -> String showList :: [THF_formula] -> ShowS | |
Generic THF_formula | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_formula :: Type -> Type | |
GetRange THF_formula Source # | |
FromJSON THF_formula | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_formula | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_formula | |
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 #
Constructors
THFLF_binary THF_binary_formula | |
THFLF_unitary THF_unitary_formula | |
THFLF_type THF_type_formula | |
THFLF_subtype THF_subtype |
Instances
Eq THF_logic_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_logic_formula -> THF_logic_formula -> Bool (/=) :: THF_logic_formula -> THF_logic_formula -> Bool | |
Data THF_logic_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_logic_formula -> THF_logic_formula -> Ordering (<) :: THF_logic_formula -> THF_logic_formula -> Bool (<=) :: THF_logic_formula -> THF_logic_formula -> Bool (>) :: THF_logic_formula -> THF_logic_formula -> Bool (>=) :: THF_logic_formula -> THF_logic_formula -> Bool max :: THF_logic_formula -> THF_logic_formula -> THF_logic_formula min :: THF_logic_formula -> THF_logic_formula -> THF_logic_formula | |
Show THF_logic_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_logic_formula :: Type -> Type Methods from :: THF_logic_formula -> Rep THF_logic_formula x to :: Rep THF_logic_formula x -> THF_logic_formula | |
GetRange THF_logic_formula Source # | |
FromJSON THF_logic_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_logic_formula parseJSONList :: Value -> Parser [THF_logic_formula] | |
ToJSON THF_logic_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_logic_formula -> Value toEncoding :: THF_logic_formula -> Encoding toJSONList :: [THF_logic_formula] -> Value toEncodingList :: [THF_logic_formula] -> Encoding | |
ShATermConvertible THF_logic_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_logic_formula | |
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 #
Constructors
THFBF_pair THF_binary_pair | |
THFBF_tuple THF_binary_tuple |
Instances
Eq THF_binary_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_binary_formula -> THF_binary_formula -> Bool (/=) :: THF_binary_formula -> THF_binary_formula -> Bool | |
Data THF_binary_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_binary_formula -> THF_binary_formula -> Ordering (<) :: THF_binary_formula -> THF_binary_formula -> Bool (<=) :: THF_binary_formula -> THF_binary_formula -> Bool (>) :: THF_binary_formula -> THF_binary_formula -> Bool (>=) :: THF_binary_formula -> THF_binary_formula -> Bool max :: THF_binary_formula -> THF_binary_formula -> THF_binary_formula min :: THF_binary_formula -> THF_binary_formula -> THF_binary_formula | |
Show THF_binary_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_binary_formula :: Type -> Type Methods from :: THF_binary_formula -> Rep THF_binary_formula x to :: Rep THF_binary_formula x -> THF_binary_formula | |
GetRange THF_binary_formula Source # | |
FromJSON THF_binary_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_binary_formula parseJSONList :: Value -> Parser [THF_binary_formula] | |
ToJSON THF_binary_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_binary_formula -> Value toEncoding :: THF_binary_formula -> Encoding toJSONList :: [THF_binary_formula] -> Value toEncodingList :: [THF_binary_formula] -> Encoding | |
ShATermConvertible THF_binary_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_binary_formula | |
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
Eq THF_binary_pair Source # | |
Defined in TPTP.AS Methods (==) :: THF_binary_pair -> THF_binary_pair -> Bool (/=) :: THF_binary_pair -> THF_binary_pair -> Bool | |
Data THF_binary_pair Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_binary_pair -> THF_binary_pair -> Ordering (<) :: THF_binary_pair -> THF_binary_pair -> Bool (<=) :: THF_binary_pair -> THF_binary_pair -> Bool (>) :: THF_binary_pair -> THF_binary_pair -> Bool (>=) :: THF_binary_pair -> THF_binary_pair -> Bool max :: THF_binary_pair -> THF_binary_pair -> THF_binary_pair min :: THF_binary_pair -> THF_binary_pair -> THF_binary_pair | |
Show THF_binary_pair Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_binary_pair :: Type -> Type Methods from :: THF_binary_pair -> Rep THF_binary_pair x to :: Rep THF_binary_pair x -> THF_binary_pair | |
GetRange THF_binary_pair Source # | |
FromJSON THF_binary_pair | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_binary_pair parseJSONList :: Value -> Parser [THF_binary_pair] | |
ToJSON THF_binary_pair | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_binary_pair | |
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
Eq THF_binary_tuple Source # | |
Defined in TPTP.AS Methods (==) :: THF_binary_tuple -> THF_binary_tuple -> Bool (/=) :: THF_binary_tuple -> THF_binary_tuple -> Bool | |
Data THF_binary_tuple Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_binary_tuple -> THF_binary_tuple -> Ordering (<) :: THF_binary_tuple -> THF_binary_tuple -> Bool (<=) :: THF_binary_tuple -> THF_binary_tuple -> Bool (>) :: THF_binary_tuple -> THF_binary_tuple -> Bool (>=) :: THF_binary_tuple -> THF_binary_tuple -> Bool max :: THF_binary_tuple -> THF_binary_tuple -> THF_binary_tuple min :: THF_binary_tuple -> THF_binary_tuple -> THF_binary_tuple | |
Show THF_binary_tuple Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_binary_tuple :: Type -> Type Methods from :: THF_binary_tuple -> Rep THF_binary_tuple x to :: Rep THF_binary_tuple x -> THF_binary_tuple | |
GetRange THF_binary_tuple Source # | |
FromJSON THF_binary_tuple | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_binary_tuple parseJSONList :: Value -> Parser [THF_binary_tuple] | |
ToJSON THF_binary_tuple | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_binary_tuple -> Value toEncoding :: THF_binary_tuple -> Encoding toJSONList :: [THF_binary_tuple] -> Value toEncodingList :: [THF_binary_tuple] -> Encoding | |
ShATermConvertible THF_binary_tuple | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_binary_tuple | |
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)))) |
type THF_or_formula = [THF_unitary_formula] Source #
type THF_and_formula = [THF_unitary_formula] Source #
type THF_apply_formula = [THF_unitary_formula] Source #
data THF_unitary_formula Source #
Constructors
THFUF_quantified THF_quantified_formula | |
THFUF_unary THF_unary_formula | |
THFUF_atom THF_atom | |
THFUF_conditional THF_conditional | |
THFUF_let THF_let | |
THFUF_tuple THF_tuple | |
THFUF_logic THF_logic_formula |
Instances
Eq THF_unitary_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_unitary_formula -> THF_unitary_formula -> Bool (/=) :: THF_unitary_formula -> THF_unitary_formula -> Bool | |
Data THF_unitary_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_unitary_formula -> THF_unitary_formula -> Ordering (<) :: THF_unitary_formula -> THF_unitary_formula -> Bool (<=) :: THF_unitary_formula -> THF_unitary_formula -> Bool (>) :: THF_unitary_formula -> THF_unitary_formula -> Bool (>=) :: THF_unitary_formula -> THF_unitary_formula -> Bool max :: THF_unitary_formula -> THF_unitary_formula -> THF_unitary_formula min :: THF_unitary_formula -> THF_unitary_formula -> THF_unitary_formula | |
Show THF_unitary_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_unitary_formula :: Type -> Type Methods from :: THF_unitary_formula -> Rep THF_unitary_formula x to :: Rep THF_unitary_formula x -> THF_unitary_formula | |
GetRange THF_unitary_formula Source # | |
FromJSON THF_unitary_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_unitary_formula parseJSONList :: Value -> Parser [THF_unitary_formula] | |
ToJSON THF_unitary_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_unitary_formula -> Value toEncoding :: THF_unitary_formula -> Encoding toJSONList :: [THF_unitary_formula] -> Value toEncodingList :: [THF_unitary_formula] -> Encoding | |
ShATermConvertible THF_unitary_formula | |
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 # | |
Defined in TPTP.Pretty Methods pretty :: THF_unitary_formula -> Doc Source # pretties :: [THF_unitary_formula] -> Doc Source # | |
type Rep THF_unitary_formula | |
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
data THF_quantification Source #
Constructors
THF_quantification THF_quantifier THF_variable_list |
Instances
Eq THF_quantification Source # | |
Defined in TPTP.AS Methods (==) :: THF_quantification -> THF_quantification -> Bool (/=) :: THF_quantification -> THF_quantification -> Bool | |
Data THF_quantification Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_quantification -> THF_quantification -> Ordering (<) :: THF_quantification -> THF_quantification -> Bool (<=) :: THF_quantification -> THF_quantification -> Bool (>) :: THF_quantification -> THF_quantification -> Bool (>=) :: THF_quantification -> THF_quantification -> Bool max :: THF_quantification -> THF_quantification -> THF_quantification min :: THF_quantification -> THF_quantification -> THF_quantification | |
Show THF_quantification Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_quantification -> ShowS show :: THF_quantification -> String showList :: [THF_quantification] -> ShowS | |
Generic THF_quantification | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_quantification :: Type -> Type Methods from :: THF_quantification -> Rep THF_quantification x to :: Rep THF_quantification x -> THF_quantification | |
GetRange THF_quantification Source # | |
FromJSON THF_quantification | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_quantification parseJSONList :: Value -> Parser [THF_quantification] | |
ToJSON THF_quantification | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_quantification -> Value toEncoding :: THF_quantification -> Encoding toJSONList :: [THF_quantification] -> Value toEncodingList :: [THF_quantification] -> Encoding | |
ShATermConvertible THF_quantification | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_quantification | |
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))) |
type THF_variable_list = [THF_variable] Source #
data THF_variable Source #
Constructors
THFV_typed THF_typed_variable | |
THFV_variable Variable |
Instances
Eq THF_variable Source # | |
Defined in TPTP.AS | |
Data THF_variable Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_variable -> THF_variable -> Ordering (<) :: THF_variable -> THF_variable -> Bool (<=) :: THF_variable -> THF_variable -> Bool (>) :: THF_variable -> THF_variable -> Bool (>=) :: THF_variable -> THF_variable -> Bool max :: THF_variable -> THF_variable -> THF_variable min :: THF_variable -> THF_variable -> THF_variable | |
Show THF_variable Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_variable -> ShowS show :: THF_variable -> String showList :: [THF_variable] -> ShowS | |
Generic THF_variable | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_variable :: Type -> Type | |
GetRange THF_variable Source # | |
FromJSON THF_variable | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_variable | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_variable | |
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 #
Constructors
THF_typed_variable Variable THF_top_level_type |
Instances
Eq THF_typed_variable Source # | |
Defined in TPTP.AS Methods (==) :: THF_typed_variable -> THF_typed_variable -> Bool (/=) :: THF_typed_variable -> THF_typed_variable -> Bool | |
Data THF_typed_variable Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_typed_variable -> THF_typed_variable -> Ordering (<) :: THF_typed_variable -> THF_typed_variable -> Bool (<=) :: THF_typed_variable -> THF_typed_variable -> Bool (>) :: THF_typed_variable -> THF_typed_variable -> Bool (>=) :: THF_typed_variable -> THF_typed_variable -> Bool max :: THF_typed_variable -> THF_typed_variable -> THF_typed_variable min :: THF_typed_variable -> THF_typed_variable -> THF_typed_variable | |
Show THF_typed_variable Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_typed_variable :: Type -> Type Methods from :: THF_typed_variable -> Rep THF_typed_variable x to :: Rep THF_typed_variable x -> THF_typed_variable | |
GetRange THF_typed_variable Source # | |
FromJSON THF_typed_variable | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_typed_variable parseJSONList :: Value -> Parser [THF_typed_variable] | |
ToJSON THF_typed_variable | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_typed_variable -> Value toEncoding :: THF_typed_variable -> Encoding toJSONList :: [THF_typed_variable] -> Value toEncodingList :: [THF_typed_variable] -> Encoding | |
ShATermConvertible THF_typed_variable | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_typed_variable | |
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 #
Constructors
THF_unary_formula THF_unary_connective THF_logic_formula |
Instances
Eq THF_unary_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_unary_formula -> THF_unary_formula -> Bool (/=) :: THF_unary_formula -> THF_unary_formula -> Bool | |
Data THF_unary_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_unary_formula -> THF_unary_formula -> Ordering (<) :: THF_unary_formula -> THF_unary_formula -> Bool (<=) :: THF_unary_formula -> THF_unary_formula -> Bool (>) :: THF_unary_formula -> THF_unary_formula -> Bool (>=) :: THF_unary_formula -> THF_unary_formula -> Bool max :: THF_unary_formula -> THF_unary_formula -> THF_unary_formula min :: THF_unary_formula -> THF_unary_formula -> THF_unary_formula | |
Show THF_unary_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_unary_formula :: Type -> Type Methods from :: THF_unary_formula -> Rep THF_unary_formula x to :: Rep THF_unary_formula x -> THF_unary_formula | |
GetRange THF_unary_formula Source # | |
FromJSON THF_unary_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_unary_formula parseJSONList :: Value -> Parser [THF_unary_formula] | |
ToJSON THF_unary_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_unary_formula -> Value toEncoding :: THF_unary_formula -> Encoding toJSONList :: [THF_unary_formula] -> Value toEncodingList :: [THF_unary_formula] -> Encoding | |
ShATermConvertible THF_unary_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_unary_formula | |
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))) |
Constructors
THF_atom_function THF_function | |
THF_atom_variable Variable | |
THF_atom_defined Defined_term | |
THF_atom_conn THF_conn_term |
Instances
Eq THF_atom Source # | |
Data THF_atom Source # | |
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 # | |
Show THF_atom Source # | |
Generic THF_atom | |
GetRange THF_atom Source # | |
FromJSON THF_atom | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_atom | |
Defined in TPTP.ATC_TPTP Methods toEncoding :: THF_atom -> Encoding toJSONList :: [THF_atom] -> Value toEncodingList :: [THF_atom] -> Encoding | |
ShATermConvertible THF_atom | |
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 # | |
type Rep THF_atom | |
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 #
Constructors
THFF_atom Atom | |
THFF_functor TPTP_functor THF_arguments | |
THFF_defined Defined_functor THF_arguments | |
THFF_system System_functor THF_arguments |
Instances
Eq THF_function Source # | |
Defined in TPTP.AS | |
Data THF_function Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_function -> THF_function -> Ordering (<) :: THF_function -> THF_function -> Bool (<=) :: THF_function -> THF_function -> Bool (>) :: THF_function -> THF_function -> Bool (>=) :: THF_function -> THF_function -> Bool max :: THF_function -> THF_function -> THF_function min :: THF_function -> THF_function -> THF_function | |
Show THF_function Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_function -> ShowS show :: THF_function -> String showList :: [THF_function] -> ShowS | |
Generic THF_function | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_function :: Type -> Type | |
GetRange THF_function Source # | |
FromJSON THF_function | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_function | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_function | |
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 #
Constructors
THFC_pair THF_pair_connective | |
THFC_assoc Assoc_connective | |
THFC_unary THF_unary_connective |
Instances
Eq THF_conn_term Source # | |
Defined in TPTP.AS | |
Data THF_conn_term Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_conn_term -> THF_conn_term -> Ordering (<) :: THF_conn_term -> THF_conn_term -> Bool (<=) :: THF_conn_term -> THF_conn_term -> Bool (>) :: THF_conn_term -> THF_conn_term -> Bool (>=) :: THF_conn_term -> THF_conn_term -> Bool max :: THF_conn_term -> THF_conn_term -> THF_conn_term min :: THF_conn_term -> THF_conn_term -> THF_conn_term | |
Show THF_conn_term Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_conn_term :: Type -> Type | |
GetRange THF_conn_term Source # | |
FromJSON THF_conn_term | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_conn_term | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_conn_term | |
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
Eq THF_conditional Source # | |
Defined in TPTP.AS Methods (==) :: THF_conditional -> THF_conditional -> Bool (/=) :: THF_conditional -> THF_conditional -> Bool | |
Data THF_conditional Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_conditional -> THF_conditional -> Ordering (<) :: THF_conditional -> THF_conditional -> Bool (<=) :: THF_conditional -> THF_conditional -> Bool (>) :: THF_conditional -> THF_conditional -> Bool (>=) :: THF_conditional -> THF_conditional -> Bool max :: THF_conditional -> THF_conditional -> THF_conditional min :: THF_conditional -> THF_conditional -> THF_conditional | |
Show THF_conditional Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_conditional -> ShowS show :: THF_conditional -> String showList :: [THF_conditional] -> ShowS | |
Generic THF_conditional | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_conditional :: Type -> Type Methods from :: THF_conditional -> Rep THF_conditional x to :: Rep THF_conditional x -> THF_conditional | |
GetRange THF_conditional Source # | |
FromJSON THF_conditional | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_conditional parseJSONList :: Value -> Parser [THF_conditional] | |
ToJSON THF_conditional | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_conditional | |
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)))) |
Constructors
THF_let THF_let_defns THF_formula |
Instances
Eq THF_let Source # | |
Data THF_let Source # | |
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 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 # | |
Show THF_let Source # | |
Generic THF_let | |
GetRange THF_let Source # | |
FromJSON THF_let | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_let | |
Defined in TPTP.ATC_TPTP Methods toEncoding :: THF_let -> Encoding toJSONList :: [THF_let] -> Value toEncodingList :: [THF_let] -> Encoding | |
ShATermConvertible THF_let | |
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 # | |
type Rep THF_let | |
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 #
Constructors
THFLD_single THF_let_defn | |
THFLD_many THF_let_defn_list |
Instances
Eq THF_let_defns Source # | |
Defined in TPTP.AS | |
Data THF_let_defns Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_let_defns -> THF_let_defns -> Ordering (<) :: THF_let_defns -> THF_let_defns -> Bool (<=) :: THF_let_defns -> THF_let_defns -> Bool (>) :: THF_let_defns -> THF_let_defns -> Bool (>=) :: THF_let_defns -> THF_let_defns -> Bool max :: THF_let_defns -> THF_let_defns -> THF_let_defns min :: THF_let_defns -> THF_let_defns -> THF_let_defns | |
Show THF_let_defns Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_let_defns :: Type -> Type | |
GetRange THF_let_defns Source # | |
FromJSON THF_let_defns | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_let_defns | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_let_defns | |
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))) |
type THF_let_defn_list = [THF_let_defn] Source #
data THF_let_defn Source #
Instances
Eq THF_let_defn Source # | |
Defined in TPTP.AS | |
Data THF_let_defn Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_let_defn -> THF_let_defn -> Ordering (<) :: THF_let_defn -> THF_let_defn -> Bool (<=) :: THF_let_defn -> THF_let_defn -> Bool (>) :: THF_let_defn -> THF_let_defn -> Bool (>=) :: THF_let_defn -> THF_let_defn -> Bool max :: THF_let_defn -> THF_let_defn -> THF_let_defn min :: THF_let_defn -> THF_let_defn -> THF_let_defn | |
Show THF_let_defn Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_let_defn :: Type -> Type | |
GetRange THF_let_defn Source # | |
FromJSON THF_let_defn | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_let_defn | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_let_defn | |
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
data THF_let_plain_defn Source #
Constructors
THF_let_plain_defn THF_let_defn_LHS THF_formula |
Instances
Eq THF_let_plain_defn Source # | |
Defined in TPTP.AS Methods (==) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (/=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool | |
Data THF_let_plain_defn Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_let_plain_defn -> THF_let_plain_defn -> Ordering (<) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (<=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (>) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool (>=) :: THF_let_plain_defn -> THF_let_plain_defn -> Bool max :: THF_let_plain_defn -> THF_let_plain_defn -> THF_let_plain_defn min :: THF_let_plain_defn -> THF_let_plain_defn -> THF_let_plain_defn | |
Show THF_let_plain_defn Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_let_plain_defn :: Type -> Type Methods from :: THF_let_plain_defn -> Rep THF_let_plain_defn x to :: Rep THF_let_plain_defn x -> THF_let_plain_defn | |
GetRange THF_let_plain_defn Source # | |
FromJSON THF_let_plain_defn | |
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 | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_let_plain_defn -> Value toEncoding :: THF_let_plain_defn -> Encoding toJSONList :: [THF_let_plain_defn] -> Value toEncodingList :: [THF_let_plain_defn] -> Encoding | |
ShATermConvertible THF_let_plain_defn | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_let_plain_defn | |
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 #
Constructors
THFLDL_constant Constant | |
THFLDL_functor TPTP_functor FOF_arguments | |
THFLDL_tuple THF_tuple |
Instances
Eq THF_let_defn_LHS Source # | |
Defined in TPTP.AS Methods (==) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (/=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool | |
Data THF_let_defn_LHS Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_let_defn_LHS -> THF_let_defn_LHS -> Ordering (<) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (<=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (>) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool (>=) :: THF_let_defn_LHS -> THF_let_defn_LHS -> Bool max :: THF_let_defn_LHS -> THF_let_defn_LHS -> THF_let_defn_LHS min :: THF_let_defn_LHS -> THF_let_defn_LHS -> THF_let_defn_LHS | |
Show THF_let_defn_LHS Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_let_defn_LHS :: Type -> Type Methods from :: THF_let_defn_LHS -> Rep THF_let_defn_LHS x to :: Rep THF_let_defn_LHS x -> THF_let_defn_LHS | |
GetRange THF_let_defn_LHS Source # | |
FromJSON THF_let_defn_LHS | |
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 | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_let_defn_LHS -> Value toEncoding :: THF_let_defn_LHS -> Encoding toJSONList :: [THF_let_defn_LHS] -> Value toEncodingList :: [THF_let_defn_LHS] -> Encoding | |
ShATermConvertible THF_let_defn_LHS | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_let_defn_LHS | |
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)))) |
type THF_arguments = THF_formula_list Source #
data THF_type_formula Source #
Constructors
THFTF_typeable THF_typeable_formula THF_top_level_type | |
THFTF_constant Constant THF_top_level_type |
Instances
Eq THF_type_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_type_formula -> THF_type_formula -> Bool (/=) :: THF_type_formula -> THF_type_formula -> Bool | |
Data THF_type_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_type_formula -> THF_type_formula -> Ordering (<) :: THF_type_formula -> THF_type_formula -> Bool (<=) :: THF_type_formula -> THF_type_formula -> Bool (>) :: THF_type_formula -> THF_type_formula -> Bool (>=) :: THF_type_formula -> THF_type_formula -> Bool max :: THF_type_formula -> THF_type_formula -> THF_type_formula min :: THF_type_formula -> THF_type_formula -> THF_type_formula | |
Show THF_type_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_type_formula :: Type -> Type Methods from :: THF_type_formula -> Rep THF_type_formula x to :: Rep THF_type_formula x -> THF_type_formula | |
GetRange THF_type_formula Source # | |
FromJSON THF_type_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_type_formula parseJSONList :: Value -> Parser [THF_type_formula] | |
ToJSON THF_type_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_type_formula -> Value toEncoding :: THF_type_formula -> Encoding toJSONList :: [THF_type_formula] -> Value toEncodingList :: [THF_type_formula] -> Encoding | |
ShATermConvertible THF_type_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_type_formula | |
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 #
Constructors
THFTF_atom THF_atom | |
THFTF_logic THF_logic_formula |
Instances
Eq THF_typeable_formula Source # | |
Defined in TPTP.AS Methods (==) :: THF_typeable_formula -> THF_typeable_formula -> Bool (/=) :: THF_typeable_formula -> THF_typeable_formula -> Bool | |
Data THF_typeable_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_typeable_formula -> THF_typeable_formula -> Ordering (<) :: THF_typeable_formula -> THF_typeable_formula -> Bool (<=) :: THF_typeable_formula -> THF_typeable_formula -> Bool (>) :: THF_typeable_formula -> THF_typeable_formula -> Bool (>=) :: THF_typeable_formula -> THF_typeable_formula -> Bool max :: THF_typeable_formula -> THF_typeable_formula -> THF_typeable_formula min :: THF_typeable_formula -> THF_typeable_formula -> THF_typeable_formula | |
Show THF_typeable_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_typeable_formula :: Type -> Type Methods from :: THF_typeable_formula -> Rep THF_typeable_formula x to :: Rep THF_typeable_formula x -> THF_typeable_formula | |
GetRange THF_typeable_formula Source # | |
FromJSON THF_typeable_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_typeable_formula parseJSONList :: Value -> Parser [THF_typeable_formula] | |
ToJSON THF_typeable_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_typeable_formula -> Value toEncoding :: THF_typeable_formula -> Encoding toJSONList :: [THF_typeable_formula] -> Value toEncodingList :: [THF_typeable_formula] -> Encoding | |
ShATermConvertible THF_typeable_formula | |
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 # | |
Defined in TPTP.Pretty Methods pretty :: THF_typeable_formula -> Doc Source # pretties :: [THF_typeable_formula] -> Doc Source # | |
type Rep THF_typeable_formula | |
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 #
Constructors
THF_subtype THF_atom THF_atom |
Instances
Eq THF_subtype Source # | |
Defined in TPTP.AS | |
Data THF_subtype Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_subtype -> THF_subtype -> Ordering (<) :: THF_subtype -> THF_subtype -> Bool (<=) :: THF_subtype -> THF_subtype -> Bool (>) :: THF_subtype -> THF_subtype -> Bool (>=) :: THF_subtype -> THF_subtype -> Bool max :: THF_subtype -> THF_subtype -> THF_subtype min :: THF_subtype -> THF_subtype -> THF_subtype | |
Show THF_subtype Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_subtype -> ShowS show :: THF_subtype -> String showList :: [THF_subtype] -> ShowS | |
Generic THF_subtype | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_subtype :: Type -> Type | |
GetRange THF_subtype Source # | |
FromJSON THF_subtype | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_subtype | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_subtype | |
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 #
Constructors
THFTLT_unitary THF_unitary_type | |
THFTLT_mapping THF_mapping_type |
Instances
Eq THF_top_level_type Source # | |
Defined in TPTP.AS Methods (==) :: THF_top_level_type -> THF_top_level_type -> Bool (/=) :: THF_top_level_type -> THF_top_level_type -> Bool | |
Data THF_top_level_type Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_top_level_type -> THF_top_level_type -> Ordering (<) :: THF_top_level_type -> THF_top_level_type -> Bool (<=) :: THF_top_level_type -> THF_top_level_type -> Bool (>) :: THF_top_level_type -> THF_top_level_type -> Bool (>=) :: THF_top_level_type -> THF_top_level_type -> Bool max :: THF_top_level_type -> THF_top_level_type -> THF_top_level_type min :: THF_top_level_type -> THF_top_level_type -> THF_top_level_type | |
Show THF_top_level_type Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_top_level_type :: Type -> Type Methods from :: THF_top_level_type -> Rep THF_top_level_type x to :: Rep THF_top_level_type x -> THF_top_level_type | |
GetRange THF_top_level_type Source # | |
FromJSON THF_top_level_type | |
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 | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_top_level_type -> Value toEncoding :: THF_top_level_type -> Encoding toJSONList :: [THF_top_level_type] -> Value toEncodingList :: [THF_top_level_type] -> Encoding | |
ShATermConvertible THF_top_level_type | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_top_level_type | |
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 #
Constructors
THFUT_unitary THF_unitary_formula | |
THFUT_binary THF_binary_type |
Instances
Eq THF_unitary_type Source # | |
Defined in TPTP.AS Methods (==) :: THF_unitary_type -> THF_unitary_type -> Bool (/=) :: THF_unitary_type -> THF_unitary_type -> Bool | |
Data THF_unitary_type Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_unitary_type -> THF_unitary_type -> Ordering (<) :: THF_unitary_type -> THF_unitary_type -> Bool (<=) :: THF_unitary_type -> THF_unitary_type -> Bool (>) :: THF_unitary_type -> THF_unitary_type -> Bool (>=) :: THF_unitary_type -> THF_unitary_type -> Bool max :: THF_unitary_type -> THF_unitary_type -> THF_unitary_type min :: THF_unitary_type -> THF_unitary_type -> THF_unitary_type | |
Show THF_unitary_type Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_unitary_type :: Type -> Type Methods from :: THF_unitary_type -> Rep THF_unitary_type x to :: Rep THF_unitary_type x -> THF_unitary_type | |
GetRange THF_unitary_type Source # | |
FromJSON THF_unitary_type | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_unitary_type parseJSONList :: Value -> Parser [THF_unitary_type] | |
ToJSON THF_unitary_type | |
Defined in TPTP.ATC_TPTP Methods toJSON :: THF_unitary_type -> Value toEncoding :: THF_unitary_type -> Encoding toJSONList :: [THF_unitary_type] -> Value toEncodingList :: [THF_unitary_type] -> Encoding | |
ShATermConvertible THF_unitary_type | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_unitary_type | |
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
Eq THF_binary_type Source # | |
Defined in TPTP.AS Methods (==) :: THF_binary_type -> THF_binary_type -> Bool (/=) :: THF_binary_type -> THF_binary_type -> Bool | |
Data THF_binary_type Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_binary_type -> THF_binary_type -> Ordering (<) :: THF_binary_type -> THF_binary_type -> Bool (<=) :: THF_binary_type -> THF_binary_type -> Bool (>) :: THF_binary_type -> THF_binary_type -> Bool (>=) :: THF_binary_type -> THF_binary_type -> Bool max :: THF_binary_type -> THF_binary_type -> THF_binary_type min :: THF_binary_type -> THF_binary_type -> THF_binary_type | |
Show THF_binary_type Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_binary_type :: Type -> Type Methods from :: THF_binary_type -> Rep THF_binary_type x to :: Rep THF_binary_type x -> THF_binary_type | |
GetRange THF_binary_type Source # | |
FromJSON THF_binary_type | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser THF_binary_type parseJSONList :: Value -> Parser [THF_binary_type] | |
ToJSON THF_binary_type | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_binary_type | |
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)))) |
type THF_mapping_type = [THF_unitary_type] Source #
type THF_xprod_type = [THF_unitary_type] Source #
type THF_union_type = [THF_unitary_type] Source #
data THF_sequent Source #
Constructors
THFS_plain THF_tuple THF_tuple | |
THFS_parens THF_sequent |
Instances
Eq THF_sequent Source # | |
Defined in TPTP.AS | |
Data THF_sequent Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: THF_sequent -> THF_sequent -> Ordering (<) :: THF_sequent -> THF_sequent -> Bool (<=) :: THF_sequent -> THF_sequent -> Bool (>) :: THF_sequent -> THF_sequent -> Bool (>=) :: THF_sequent -> THF_sequent -> Bool max :: THF_sequent -> THF_sequent -> THF_sequent min :: THF_sequent -> THF_sequent -> THF_sequent | |
Show THF_sequent Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> THF_sequent -> ShowS show :: THF_sequent -> String showList :: [THF_sequent] -> ShowS | |
Generic THF_sequent | |
Defined in TPTP.ATC_TPTP Associated Types type Rep THF_sequent :: Type -> Type | |
GetRange THF_sequent Source # | |
FromJSON THF_sequent | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_sequent | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep THF_sequent | |
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))) |
Constructors
THF_tuple THF_formula_list |
Instances
Eq THF_tuple Source # | |
Data THF_tuple Source # | |
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 # | |
Defined in TPTP.AS | |
Show THF_tuple Source # | |
Generic THF_tuple | |
GetRange THF_tuple Source # | |
FromJSON THF_tuple | |
Defined in TPTP.ATC_TPTP | |
ToJSON THF_tuple | |
Defined in TPTP.ATC_TPTP Methods toEncoding :: THF_tuple -> Encoding toJSONList :: [THF_tuple] -> Value toEncodingList :: [THF_tuple] -> Encoding | |
ShATermConvertible THF_tuple | |
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 # | |
type Rep THF_tuple | |
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))) |
type THF_formula_list = [THF_logic_formula] Source #
data TFX_formula Source #
Constructors
TFXF_logic TFX_logic_formula | |
TFXF_sequent THF_sequent |
Instances
Eq TFX_formula Source # | |
Defined in TPTP.AS | |
Data TFX_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFX_formula -> TFX_formula -> Ordering (<) :: TFX_formula -> TFX_formula -> Bool (<=) :: TFX_formula -> TFX_formula -> Bool (>) :: TFX_formula -> TFX_formula -> Bool (>=) :: TFX_formula -> TFX_formula -> Bool max :: TFX_formula -> TFX_formula -> TFX_formula min :: TFX_formula -> TFX_formula -> TFX_formula | |
Show TFX_formula Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TFX_formula -> ShowS show :: TFX_formula -> String showList :: [TFX_formula] -> ShowS | |
Generic TFX_formula | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFX_formula :: Type -> Type | |
GetRange TFX_formula Source # | |
FromJSON TFX_formula | |
Defined in TPTP.ATC_TPTP | |
ToJSON TFX_formula | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFX_formula | |
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 #
Constructors
TFXLF_binary THF_binary_formula | |
TFXLF_unitary THF_unitary_formula | |
TFXLF_typed TFF_typed_atom | |
TFXLF_subtype TFF_subtype |
Instances
Eq TFX_logic_formula Source # | |
Defined in TPTP.AS Methods (==) :: TFX_logic_formula -> TFX_logic_formula -> Bool (/=) :: TFX_logic_formula -> TFX_logic_formula -> Bool | |
Data TFX_logic_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFX_logic_formula -> TFX_logic_formula -> Ordering (<) :: TFX_logic_formula -> TFX_logic_formula -> Bool (<=) :: TFX_logic_formula -> TFX_logic_formula -> Bool (>) :: TFX_logic_formula -> TFX_logic_formula -> Bool (>=) :: TFX_logic_formula -> TFX_logic_formula -> Bool max :: TFX_logic_formula -> TFX_logic_formula -> TFX_logic_formula min :: TFX_logic_formula -> TFX_logic_formula -> TFX_logic_formula | |
Show TFX_logic_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFX_logic_formula :: Type -> Type Methods from :: TFX_logic_formula -> Rep TFX_logic_formula x to :: Rep TFX_logic_formula x -> TFX_logic_formula | |
GetRange TFX_logic_formula Source # | |
FromJSON TFX_logic_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser TFX_logic_formula parseJSONList :: Value -> Parser [TFX_logic_formula] | |
ToJSON TFX_logic_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: TFX_logic_formula -> Value toEncoding :: TFX_logic_formula -> Encoding toJSONList :: [TFX_logic_formula] -> Value toEncodingList :: [TFX_logic_formula] -> Encoding | |
ShATermConvertible TFX_logic_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFX_logic_formula | |
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
Eq TFF_formula Source # | |
Defined in TPTP.AS | |
Data TFF_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFF_formula -> TFF_formula -> Ordering (<) :: TFF_formula -> TFF_formula -> Bool (<=) :: TFF_formula -> TFF_formula -> Bool (>) :: TFF_formula -> TFF_formula -> Bool (>=) :: TFF_formula -> TFF_formula -> Bool max :: TFF_formula -> TFF_formula -> TFF_formula min :: TFF_formula -> TFF_formula -> TFF_formula | |
Show TFF_formula Source # | |
Defined in TPTP.AS Methods showsPrec :: Int -> TFF_formula -> ShowS show :: TFF_formula -> String showList :: [TFF_formula] -> ShowS | |
Generic TFF_formula | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFF_formula :: Type -> Type | |
GetRange TFF_formula Source # | |
FromJSON TFF_formula | |
Defined in TPTP.ATC_TPTP | |
ToJSON TFF_formula | |
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 | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFF_formula | |
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 #
Constructors
TFFLF_binary TFF_binary_formula | |
TFFLF_unitary TFF_unitary_formula | |
TFFLF_subtype TFF_subtype |
Instances
Eq TFF_logic_formula Source # | |
Defined in TPTP.AS Methods (==) :: TFF_logic_formula -> TFF_logic_formula -> Bool (/=) :: TFF_logic_formula -> TFF_logic_formula -> Bool | |
Data TFF_logic_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFF_logic_formula -> TFF_logic_formula -> Ordering (<) :: TFF_logic_formula -> TFF_logic_formula -> Bool (<=) :: TFF_logic_formula -> TFF_logic_formula -> Bool (>) :: TFF_logic_formula -> TFF_logic_formula -> Bool (>=) :: TFF_logic_formula -> TFF_logic_formula -> Bool max :: TFF_logic_formula -> TFF_logic_formula -> TFF_logic_formula min :: TFF_logic_formula -> TFF_logic_formula -> TFF_logic_formula | |
Show TFF_logic_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFF_logic_formula :: Type -> Type Methods from :: TFF_logic_formula -> Rep TFF_logic_formula x to :: Rep TFF_logic_formula x -> TFF_logic_formula | |
GetRange TFF_logic_formula Source # | |
FromJSON TFF_logic_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser TFF_logic_formula parseJSONList :: Value -> Parser [TFF_logic_formula] | |
ToJSON TFF_logic_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: TFF_logic_formula -> Value toEncoding :: TFF_logic_formula -> Encoding toJSONList :: [TFF_logic_formula] -> Value toEncodingList :: [TFF_logic_formula] -> Encoding | |
ShATermConvertible TFF_logic_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFF_logic_formula | |
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 #
Constructors
TFFBF_nonassoc TFF_binary_nonassoc | |
TFFBF_assoc TFF_binary_assoc |
Instances
Eq TFF_binary_formula Source # | |
Defined in TPTP.AS Methods (==) :: TFF_binary_formula -> TFF_binary_formula -> Bool (/=) :: TFF_binary_formula -> TFF_binary_formula -> Bool | |
Data TFF_binary_formula Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFF_binary_formula -> TFF_binary_formula -> Ordering (<) :: TFF_binary_formula -> TFF_binary_formula -> Bool (<=) :: TFF_binary_formula -> TFF_binary_formula -> Bool (>) :: TFF_binary_formula -> TFF_binary_formula -> Bool (>=) :: TFF_binary_formula -> TFF_binary_formula -> Bool max :: TFF_binary_formula -> TFF_binary_formula -> TFF_binary_formula min :: TFF_binary_formula -> TFF_binary_formula -> TFF_binary_formula | |
Show TFF_binary_formula Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFF_binary_formula :: Type -> Type Methods from :: TFF_binary_formula -> Rep TFF_binary_formula x to :: Rep TFF_binary_formula x -> TFF_binary_formula | |
GetRange TFF_binary_formula Source # | |
FromJSON TFF_binary_formula | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser TFF_binary_formula parseJSONList :: Value -> Parser [TFF_binary_formula] | |
ToJSON TFF_binary_formula | |
Defined in TPTP.ATC_TPTP Methods toJSON :: TFF_binary_formula -> Value toEncoding :: TFF_binary_formula -> Encoding toJSONList :: [TFF_binary_formula] -> Value toEncodingList :: [TFF_binary_formula] -> Encoding | |
ShATermConvertible TFF_binary_formula | |
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 # | |
Defined in TPTP.Pretty | |
type Rep TFF_binary_formula | |
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
Eq TFF_binary_nonassoc Source # | |
Defined in TPTP.AS Methods (==) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (/=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool | |
Data TFF_binary_nonassoc Source # | |
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 # | |
Defined in TPTP.AS Methods compare :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Ordering (<) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (<=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (>) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool (>=) :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> Bool max :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> TFF_binary_nonassoc min :: TFF_binary_nonassoc -> TFF_binary_nonassoc -> TFF_binary_nonassoc | |
Show TFF_binary_nonassoc Source # | |
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 | |
Defined in TPTP.ATC_TPTP Associated Types type Rep TFF_binary_nonassoc :: Type -> Type Methods from :: TFF_binary_nonassoc -> Rep TFF_binary_nonassoc x to :: Rep TFF_binary_nonassoc x -> TFF_binary_nonassoc | |
GetRange TFF_binary_nonassoc Source # | |
FromJSON TFF_binary_nonassoc | |
Defined in TPTP.ATC_TPTP Methods parseJSON :: Value -> Parser TFF_binary_nonassoc parseJSONList :: Value -> Parser [TFF_binary_nonassoc] | |
ToJSON TFF_binary_nonassoc | |
Defined in TPTP.ATC_TPTP Methods toJSON :: TFF_binary_nonassoc -> Value toEncoding :: TFF_binary_nonassoc -> Encoding toJSONList :: [TFF_binary_nonassoc] -> Value toEncodingList :: [TFF_binary_nonassoc] -> Encoding | |
ShATermConvertible TFF_binary_nonassoc | |
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 # | |
Defined in TPTP.Pretty Methods pretty :: TFF_binary_nonassoc -> Doc Source # pretties :: [TFF_binary_nonassoc] -> Doc Source # | |
type Rep TFF_binary_nonassoc | |
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 #
Constructors
TFFBA_or TFF_or_formula | |
TFFBA_and TFF_and_formula |