copilot-theorem-2.2.1: k-induction for Copilot.
Copilot.Theorem.Prover.Z3
Synopsis
module Data.Default
data Options Source #
Tactics
Constructors
Fields
Instances
Methods
def :: Options #
induction :: Options -> Proof Universal Source #
kInduction :: Options -> Proof Universal Source #
onlySat :: Options -> Proof Existential Source #
onlyValidity :: Options -> Proof Universal Source #