License | GPLv2 or higher, see LICENSE.txt |
---|---|

Maintainer | Christian.Maeder@dfki.de |

Stability | provisional |

Portability | non-portable(Logic) |

Safe Haskell | None |

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