swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Raw File
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
Tip revision: b6407e0
implicitData.hs
foo1 as n:Int ~> {v:Int | v = n} -> Unit
foo1 = (0)

bar1 :: m:Int -> {z:Int | z = m} -> Unit
bar1 = (\m z -> (foo z))

foo2 as n:Int ~> {v:Int | v = (C n)} -> Unit
foo2 = (0)

bar2 :: m:Int -> {z:Int | z = (C m)} -> Unit
bar2 = (\m z -> (foo z))
back to top