Subtype.hascasl revision ab3ca4cacfada3a19ab024db7ad567b82fa1517d
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars a: -Type; b: +Type
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringtype i a b, Inj a b < a -> b
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars a: Type; b < a
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringop twice: (a ->? b) -> (a ->? b)
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringtype F a b %% should be illegal here
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars f: a ->? b; x: a
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poettering. twice f x = f (f x)
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars a: Type; b: Type
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringtype Inj a b = {f: a -> b . forall x, y: a . f x = f y => x = y}
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars a, b: Type; a < b
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringop down: b ->? a
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poettering. down (up x : b) = x
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poettering. def (down (y : b) : a) => up (down y : a) = y
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars c: Type; b < c
6a70f3aa63a3b7a6a30448c48322ad38b719cdceZbigniew Jędrzejewski-Szmek. up (up x : b) = up x : c
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poettering. up (x: a) = x: b
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringvars c, d, e, f; c < e; d < f
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringforall f: e -> f . up f : e ->? f = \ x : e . f x;
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringforall f: e ->? d . up f : c ->? f = \ x : c . up (f (up x));
12355095821fc17529af5b6eaefa31c3c520be39Lennart Poetteringforall x: c; y: d . up (x, y) : e * f = (up x, up y)