module Example where

{-@ divide' :: Int -> {v: Int | v != 0} -> Int @-}
divide' :: Int -> Int -> Int
divide' n d = n `div` d

-- liquid knows we're lying!
{-@ maybeZero :: Bool -> {v: Int | v != 0} @-}
maybeZero :: Bool -> Int
maybeZero True = 1
maybeZero False = 0

divResult = divide' 4 (maybeZero False)
-- div1 = divide' 4 1

main = print divResult