copilot-sbv-2.2.1: A compiler for CoPilot targeting SBV.

Safe HaskellNone
LanguageHaskell2010

Copilot.Compile.SBV

Synopsis

Documentation

compile :: Params -> Spec -> IO () Source #

proofACSL :: Params -> Spec -> IO () Source #

compileWithSBV :: Params -> [(String, SBVCodeGen ())] -> Spec -> IO () Source #

sbvs are optional additional SBVCodeGens to generate.

sbvDirName :: String Source #

module Copilot.Compile.SBV.Params