Documentation.SBV.Examples.Uninterpreted.Function

Demonstrates function counter-examples

Documentation

>>> -- For doctest purposes only:
>>> import Data.SBV

f :: SWord8 -> SWord8 -> SWord16

An uninterpreted function

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool

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

>>> prove thmGood
Q.E.D.