Classes_LHAssumptions.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}
module GHC.Classes_LHAssumptions where

import GHC.Types_LHAssumptions()

{-@

assume not :: x:Bool -> {v:Bool | ((v) <=> ~(x))}
define not    x                         = (~ x)

assume &&    :: x:Bool -> y:Bool
        -> {v:Bool | ((v) <=> ((x) && (y)))}
assume ||    :: x:Bool -> y:Bool
        -> {v:Bool | ((v) <=> ((x) || (y)))}
assume ==    :: (Eq  a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x = y)}
assume /=    :: (Eq  a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x != y)}
assume >     :: (Ord a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x > y)}
assume >=    :: (Ord a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x >= y)}
assume <     :: (Ord a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x < y)}
assume <=    :: (Ord a) => x:a -> y:a
        -> {v:Bool | ((v) <=> x <= y)}

assume compare :: (Ord a) => x:a -> y:a
        -> {v:Ordering | (((v = EQ) <=> (x = y)) &&
                                    ((v = LT) <=> (x < y)) &&
                                    ((v = GT) <=> (x > y))) }

assume max :: (Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }
assume min :: (Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) }

@-}