liquidProofsRebindableSyntax.hs

{-# LANGUAGE RebindableSyntax #-}

import Prelude hiding ( (>>=),(>>) )
import qualified Prelude as P
import Liquid.Haskell.ProofCombinators


{-@ (>>) :: x:a -> y:{a | y == x} -> {v:a | v == x && v == y} @-}
(>>) x y = x === y

{-@ reflect nott @-}
nott True = False
nott False = True

{-@ testProofDo :: x:Bool ->  { nott (nott x) = x } @-}
testProofDo True = toProof $ do
    nott (nott True)
    nott False
    True
testProofDo False = toProof $ do
    nott (nott False)
    nott True
    False

{-@ testProofNormal :: x:Bool ->  { nott (nott x) = x } @-}
testProofNormal True
    =   nott (nott True)
    === nott False
    === True
    *** QED
testProofNormal False
    =   nott (nott True)
    === nott False
    === True
    *** QED


main = do
    print 1