Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

30 lines (18 sloc) 0.467 kB
myid : a -> a
myid x = x
idid : (a : Set) -> a -> a
idid = myid ![myid]
app : (a -> b) -> a -> b
app f x = f x
foo : a -> b -> c -> d -> e -> e
foo a b c d e = e
doapp : a -> a
doapp x = app myid x
{-
id : (b : Set k) -> b -> b : Set l, k < l
foo = id ((a : Set k) -> a -> a) id
Set m, k < m
So we have k < m, k < l, m <= k
when converting Set m against Set n, we must have m <= n
if we can reach m from n, we have an inconsistency
-}
Jump to Line
Something went wrong with that request. Please try again.