Hets - the Heterogeneous Tool Set

LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Proofs.SimpleTheoremHideShift

Description

simple version of theorem hide shift proof rule for development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual.

Synopsis

Documentation

theoremHideShift :: LibName -> LibEnv -> LibEnv Source #

to be exported function. firstly it gets all the hiding definition links out of DGraph and passes them to theoremHideShiftFromList which does the actual processing

getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab] Source #

get all the global unproven threorem links which go into the given node in the given dgraph