    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.Function
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates function counter-examples
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.Function where

    import Data.SBV

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

    -- | An uninterpreted function
    f :: SWord8 -> SWord8 -> SWord16
    f :: SWord8 -> SWord8 -> SWord16
    f = String -> SWord8 -> SWord8 -> SWord16
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "f"

    -- | Asserts that @f x z == f (y+2) z@ whenever @x == y+2@. Naturally correct:
    --
    -- >>> prove thmGood
    -- Q.E.D.
    thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
    thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
    thmGood SWord8
    x SWord8
    y SWord8
    z = SWord8
    x SWord8 -> SWord8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SWord8
    ySWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    +SWord8
    2 SBool -> SBool -> SBool
    .=> SWord8 -> SWord8 -> SWord16
    f SWord8
    x SWord8
    z SWord16 -> SWord16 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SWord8 -> SWord8 -> SWord16
    f (SWord8
    y SWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    + SWord8
    2) SWord8
    z