cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Symbolic

Contents

Description

 
Synopsis

Documentation

data ProverCommand Source #

Constructors

ProverCommand 

Fields

data QueryType Source #

Instances
Show QueryType Source # 
Instance details

Defined in Cryptol.Symbolic

data SatNum Source #

Constructors

AllSat 
SomeSat Int 
Instances
Show SatNum Source # 
Instance details

Defined in Cryptol.Symbolic

data ProverResult Source #

A prover result is either an error message, an empty result (eg for the offline prover), a counterexample or a lazy list of satisfying assignments.

data CounterExampleType Source #

A :prove command can fail either because some input causes the predicate to violate a safety assertion, or because the predicate returns false for some input.

FinType