copilot-theorem-3.2: k-induction for Copilot.
Safe HaskellSafe
LanguageHaskell2010

Copilot.Theorem.Kind2

Documentation

toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File Source #

data Style Source #

Constructors

Inlined 
Modular 

data File Source #

Constructors

File 

Fields

data Prop Source #

Constructors

Prop 

Fields

data Type Source #

Constructors

Int 
Real 
Bool 

data StateVarFlag Source #

Constructors

FConst 

data PredType Source #

Constructors

Init 
Trans