Hets - the Heterogeneous Tool Set

CopyrightC. Maeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Proofs.FreeDefLinks

Description

compute ingoing free definition links for provers

Documentation

getCFreeDefLinks :: DGraph -> Node -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])

mkFreeDefMor :: [Named sentence] -> morphism -> morphism -> FreeDefMorphism sentence morphism

data GFreeDefMorphism

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => GFreeDefMorphism lid (FreeDefMorphism sentence morphism) 

Instances

getFreeDefMorphism :: LibEnv -> LibName -> DGraph -> [LEdge DGLinkLab] -> Maybe GFreeDefMorphism

getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]