swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
formatted for submission
Tip revision: b6407e0
incr00.hs
incr :: n:Int ~> (Int -> { v : Int | v == n }) -> { v : Int | v == n + 1 }
incr = \f -> (f 0) + 1
test1 :: { v : Int | v == 11 }
test1 = incr (\x -> 10)
test2 :: m:Int -> { v : Int | v == m+1 }
test2 = \mv -> incr (\x -> mv)