-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Examples.Proved
-- Copyright   :  (c) Nickolas Fotopoulos
-- License     :  BSD3
-- Maintainer  :  nickolas.fotopoulos@gmail.com
-- Stability   :  experimental
--
-- An example of activating sbvPlugin by wrapping types in Proved
-- instead of using an annotation.
--
-----------------------------------------------------------------------------

{-# LANGUAGE CPP #-}

#ifndef HADDOCK
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
#endif

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Plugin.Examples.Proved where

import Data.SBV.Plugin

-- | A top-level binding with its type wrapped in Proved causes sbvPlugin to
-- run a proof on the expression.
integerAssociative :: Proved (Integer -> Integer -> Integer -> Bool)
integerAssociative :: Proved (Integer -> Integer -> Integer -> Bool)
integerAssociative Integer
x Integer
y Integer
z = ((Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
z))

-- | Simple booleans can be made theorems too.
isTrue :: Proved Bool
isTrue :: Bool
isTrue = Bool
True Bool -> Bool -> Bool
|| Bool
False

{-# ANN module ("HLint: ignore Evaluate" :: String) #-}