liquidhaskell-0.9.14.1: src/Prelude_LHAssumptions.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-}
module Prelude_LHAssumptions where

import Data.Foldable_LHAssumptions()
import Data.List_LHAssumptions()
import GHC.Base_LHAssumptions()
import GHC.Classes_LHAssumptions()
import GHC.Float_LHAssumptions()
import GHC.Maybe_LHAssumptions()
import GHC.Num_LHAssumptions()
import GHC.Num.Integer_LHAssumptions()
import GHC.Real_LHAssumptions()
import Liquid.Prelude.Real_LHAssumptions()
import Liquid.Prelude.Totality_LHAssumptions()

{-@

assume error :: {v:_ | false} -> a

predicate Max V X Y = if X > Y then V = X else V = Y
predicate Min V X Y = if X < Y then V = X else V = Y

type IncrListD a D = [a]<{\x y -> (x+D) <= y}>

// BOT: Do not delete EVER!

qualif Bot(v:@(0))     { 0 = 1 }
qualif Bot(v:obj)      { 0 = 1 }
qualif Bot(v:a)        { 0 = 1 }
qualif Bot(v:bool)     { 0 = 1 }
qualif Bot(v:int)      { 0 = 1 }

qualif CmpZ(v:a)       { v <  0 }
qualif CmpZ(v:a)       { v <= 0 }
qualif CmpZ(v:a)       { v >  0 }
qualif CmpZ(v:a)       { v >= 0 }
qualif CmpZ(v:a)       { v  = 0 }
qualif CmpZ(v:a)       { v != 0 }

qualif Cmp(v:a, x:a)   { v <  x }
qualif Cmp(v:a, x:a)   { v <= x }
qualif Cmp(v:a, x:a)   { v >  x }
qualif Cmp(v:a, x:a)   { v >= x }
qualif Cmp(v:a, x:a)   { v  = x }
qualif Cmp(v:a, x:a)   { v != x }

qualif One(v:int)      { v = 1 }
qualif True1(v:Bool)    { v }
qualif False1(v:Bool)   { ~ v }

//  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
qualif Papp(v:a, p:Pred a)  { papp1 p v }

//  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
qualif Papp2(v:a, x:b, p:Pred a b)  { papp2 p v x }

//  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
qualif Papp3(v:a, x:b, y:c, p:Pred a b c)  { papp3 p v x y }

//  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
//  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])

//  REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
@-}