Copyright	C. Maeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

Proofs.FreeDefLinks

Description

compute ingoing free definition links for provers

Documentation

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

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

data GFreeDefMorphism Source #

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)

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

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