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
Inc02.hs
incr :: x:Int -> {v:Int | v == x + 1}
incr = \x -> x + 1
moo :: {v:Int | v == 8}
moo = incr 7
id :: rforall a. {v:a | True} -> {v:a | True}
id = \x -> x
bar :: {v:Int | v == 8}
bar = incr (id 7)
