Hets - the Heterogeneous Tool Set
Copyright(c) C. Maeder DFKI 2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Description

An embedding comorphism from HasCASL without subtypes to Isabelle-HOL.

Synopsis

Documentation

data PCoClTyConsHOL2PairsInIsaHOL Source #

The identity of the comorphism

Instances

Instances details
Show PCoClTyConsHOL2PairsInIsaHOL Source # 
Instance details

Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Language PCoClTyConsHOL2PairsInIsaHOL Source # 
Instance details

Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Methods

sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source #

sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source #

sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source #

minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source #

targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source #

mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source #

map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source #

map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source #

map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source #

map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source #

extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source #

is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source #

isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #

isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #