Documentation.SBV.Examples.Uninterpreted.Function

Author : Levent Erkok License : BSD3 Maintainer: [e-mail] Stability : experimental

Demonstrates function counter-examples

Documentation

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.