129 "{b. x:A}" == "RepFun(A, %x. b)" |
129 "{b. x:A}" == "RepFun(A, %x. b)" |
130 "INT x:A. B" == "Inter({B. x:A})" |
130 "INT x:A. B" == "Inter({B. x:A})" |
131 "UN x:A. B" == "Union({B. x:A})" |
131 "UN x:A. B" == "Union({B. x:A})" |
132 "PROD x:A. B" => "Pi(A, %x. B)" |
132 "PROD x:A. B" => "Pi(A, %x. B)" |
133 "SUM x:A. B" => "Sigma(A, %x. B)" |
133 "SUM x:A. B" => "Sigma(A, %x. B)" |
134 "A -> B" => "Pi(A, _K(B))" |
134 "A -> B" => "Pi(A, %_. B)" |
135 "A * B" => "Sigma(A, _K(B))" |
135 "A * B" => "Sigma(A, %_. B)" |
136 "lam x:A. f" == "Lambda(A, %x. f)" |
136 "lam x:A. f" == "Lambda(A, %x. f)" |
137 "ALL x:A. P" == "Ball(A, %x. P)" |
137 "ALL x:A. P" == "Ball(A, %x. P)" |
138 "EX x:A. P" == "Bex(A, %x. P)" |
138 "EX x:A. P" == "Bex(A, %x. P)" |
139 |
139 |
140 "<x, y, z>" == "<x, <y, z>>" |
140 "<x, y, z>" == "<x, <y, z>>" |