Commit 10c5a7ae authored by Danny Willems's avatar Danny Willems

More examples.

parent 72c35c97
\\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;;
\\B . \(y : B) . let id = \\A . \(x : A) . x in (id [A] x, id [B] y);; \\B . \(y : B) . let id = \\A . \(x : A) . x in (id [A] x, id [B] y);;
\\A . \(x : A -> A) . \(y : A) . x y;; \\A . \(x : A -> A) . \(y : A) . x y;;
\\A . \(x : A) . x;; \\A . \(x : A) . x;;
\\A . \\B . \(x : A) . \(y : B) . (x, y);; \\A . \\B . \(x : A) . \(y : B) . (x, y);;
\\A . \(x : A) . (\\A . \(x : A) . x) [A] x;; \\A . \\B . \(x : A) . \(y : B) . let p = (x, y) in proj1 p;;
\ No newline at end of file \\A . \(x : A) . (\\A . \(x : A) . x) [A] x;;
\\A . \\B . \(p : A * B) . proj1 p;;
\\A . \\B . \(p : A * B) . proj2 p;;
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment