sbv-8.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Uninterpreted.Function

Description

Demonstrates function counter-examples

Synopsis

Documentation

f :: SWord8 -> SWord8 -> SWord16 Source #

An uninterpreted function

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool Source #

Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct:

>>> prove thmGood
Q.E.D.