{-# LANGUAGE CPP #-}
#ifndef HADDOCK
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
#endif
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Plugin.Examples.Maximum where
import Data.SBV.Plugin
myMax :: Int -> Int -> Int -> Int
myMax :: Int -> Int -> Int -> Int
myMax Int
x Int
y Int
z | Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int
x
| Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int
y
| Bool
otherwise = Int
z
correct :: Proved (Int -> Int -> Int -> Bool)
correct :: Proved (Int -> Int -> Int -> Bool)
correct Int
x Int
y Int
z = Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
x Bool -> Bool -> Bool
&& Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
y Bool -> Bool -> Bool
&& Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
z
where m :: Int
m = Int -> Int -> Int -> Int
myMax Int
x Int
y Int
z