Copyright | (c) Simon Ulbricht, Uni Bremen 2010 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | tekknix@informatik.uni-bremen.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
This module provides sturctures and methods for the automatic proofs module.
Documentation
toGtkGoals :: FNode -> [Goal]
mostly for the purpose of proper display, the resulting G_theory of each FNode can be converted into a list of Goals.
goalsToPrefix :: [Goal] -> String
as a Prefix for display purpose, the ratio of proven and total goals is shown
showStatus :: FNode -> String
Displays every goal of a Node with a prefix showing the status and the goal name.
initFNodes :: [LNode DGNodeLab] -> [FNode]
gets all Nodes from the DGraph as input and creates a list of FNodes only containing Nodes to be considered. The results status field is initialised with the nodes local theory