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

Safe Haskell	Trustworthy
Language	Haskell2010

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

Default Options Source #
Methods def :: Options #

induction :: Options -> Proof Universal Source #

kInduction :: Options -> Proof Universal Source #

onlySat :: Options -> Proof Existential Source #

onlyValidity :: Options -> Proof Universal Source #