| License | GPLv2 or higher, see LICENSE.txt |
|---|---|
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable(Logic) |
| Safe Haskell | None |
Proofs.SimpleTheoremHideShift
Description
simple version of theorem hide shift proof rule for development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual.
- theoremHideShift :: LibName -> LibEnv -> LibEnv
- thmHideShift :: DGRule
- getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
Documentation
theoremHideShift :: LibName -> LibEnv -> LibEnv
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
rule name
getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
get all the global unproven threorem links which go into the given node in the given dgraph