copilot-theorem-2.2.0: k-induction for Copilot.

Safe HaskellNone
LanguageHaskell2010

Copilot.Theorem.Prover.Z3

Synopsis

Documentation

module Data.Default

data Options Source

Tactics

Constructors

Options 

Fields

nraNLSat :: Bool
 
startK :: Word32
 
maxK :: Word32
 
debug :: Bool
 

Instances

induction :: Options -> Proof Universal Source

kInduction :: Options -> Proof Universal Source

onlySat :: Options -> Proof Existential Source

onlyValidity :: Options -> Proof Universal Source