more_complex.inria 287 Bytes
Newer Older
Danny Willems's avatar
Danny Willems committed
1 2 3
\\B . \\A . \(x : A) . \(y : B) . proj1 (x, y);;
\\A . \\B . \(x : A) . \(y : B) . let p = (x, (y, (x, y))) in proj1 p;;
\\A . \\B . \(x : A) . \(y : B) . let p = (x, (y, (x, y))) in proj2 proj2 p;;
Danny Willems's avatar
Danny Willems committed
4
\\A . \(x : A) . \\B . \(y : B) . let id = \\A . \(x : A) . x in (id [A] x, id [B] y);;