sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Uninterpreted.Function

Description

Demonstrates function counter-examples

Synopsis

- f :: SWord8 -> SWord8 -> SWord16
- thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool

# 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.