Rebind.hs

{-# LANGUAGE RebindableSyntax #-}

module Rebind () where 

import Prelude hiding ((>>), (>>=), return)

(>>)   = plus
return = id 

{-@ plus :: x:Nat -> y:Nat -> {v:Nat | v = x + y} @-}
plus :: Int -> Int -> Int 
plus x y = x + y 

{-@ test :: {v:Nat | v = 100} @-}
test = do 
  1
  2
  3
  4