Copyright	(c) C. Maeder DFKI GmbH 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.ExtModal2ExtModalNoSubsorts

Description

Coding out subsorting (SubPCFOL= -> PCFOL=), following Chap. III:3.1 of the CASL Reference Manual

Synopsis

data ExtModal2ExtModalNoSubsorts = ExtModal2ExtModalNoSubsorts
projEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
projEM :: EM_FORMULA -> EM_FORMULA
injEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
injEM :: EM_FORMULA -> EM_FORMULA

Documentation

data ExtModal2ExtModalNoSubsorts Source #

The identity of the comorphism

Constructors

ExtModal2ExtModalNoSubsorts

Instances

Instances details

Show ExtModal2ExtModalNoSubsorts Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts Methods showsPrec :: Int -> ExtModal2ExtModalNoSubsorts -> ShowS show :: ExtModal2ExtModalNoSubsorts -> String showList :: [ExtModal2ExtModalNoSubsorts] -> ShowS
Language ExtModal2ExtModalNoSubsorts Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts Methods language_name :: ExtModal2ExtModalNoSubsorts -> String Source # description :: ExtModal2ExtModalNoSubsorts -> String Source #
Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalNoSubsorts Methods sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source # minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source # targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source # mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source # map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source # map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source # map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source # extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source # has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source # is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source # constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source # isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source # rps :: ExtModal2ExtModalNoSubsorts -> Bool Source # eps :: ExtModal2ExtModalNoSubsorts -> Bool Source # isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #

projEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA Source #

projEM :: EM_FORMULA -> EM_FORMULA Source #

injEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA Source #

injEM :: EM_FORMULA -> EM_FORMULA Source #