module Blank where

{-@  :: foo -> x:Int -> {v:Int | v > x} @-}
foo :: Int -> Int 
foo x = x - 1