Module ToVerifier

Exported Functions

cvBanner :: String   

usageText :: String   

main :: IO ()   

Further infos:

• might behave indeterministically

generateTheoremsForModule :: Options -> String -> IO ()   

Further infos:

• might behave indeterministically

generateTheorems :: Options -> IO ()   

Further infos:

• might behave indeterministically

generateTheorem :: Options -> (String, String) -> IO ()   

Further infos:

• might behave indeterministically

getAllTypeDecls :: Options -> [CurryProg] -> [(String, String)] -> [CTypeDecl] -> IO [CTypeDecl]   

Extract all type declarations that are refererred in the types of the given functions.

Further infos:

• partially defined

sortTypeDecls :: [CTypeDecl] -> [CTypeDecl]   

getAllFunctions :: Options -> [CFuncDecl] -> [CurryProg] -> [(String, String)] -> IO (Options, [CurryProg], [CFuncDecl])   

Extract all functions that might be called by a given function.

Further infos:

• partially defined
• might behave indeterministically

standardConstructors :: [(String, String)]   

Further infos:

• solution complete, i.e., able to compute all solutions