Hets - the Heterogeneous Tool Set

Copyright	(c) J. von Schroeder DFKI Bremen 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	J. von Schroeder <jonathan.von_schroeder@dfki.de>
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.THFP_P2THFP

Description

The comorphism from THFP to THF0.

Documentation

data THFP_P2THFP Source #

Constructors

Instances

Instances details

Show THFP_P2THFP Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods showsPrec :: Int -> THFP_P2THFP -> ShowS show :: THFP_P2THFP -> String showList :: [THFP_P2THFP] -> ShowS
Language THFP_P2THFP Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods language_name :: THFP_P2THFP -> String Source # description :: THFP_P2THFP -> String Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source # isGTC :: THFP_P2THFP -> Bool Source #

trans_theory :: (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #