--- a/src/CTT/CTT.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/CTT/CTT.thy Fri May 21 21:14:18 2004 +0200
@@ -34,6 +34,8 @@
split :: "[i, [i,i]=>i] =>i"
(*General Product and Function Space*)
Prod :: "[t, i=>t]=>t"
+ (*Types*)
+ "+" :: "[t,t]=>t" (infixr 40)
(*Equality type*)
Eq :: "[t,i,i]=>t"
eq :: "i"
@@ -44,12 +46,7 @@
Eqelem :: "[i,i,t]=>prop" ("(_ =/ _ :/ _)" [10,10,10] 5)
Reduce :: "[i,i]=>prop" ("Reduce[_,_]")
(*Types*)
- "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
- "+" :: "[t,t]=>t" (infixr 40)
- (*Invisible infixes!*)
- "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30)
- "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50)
+
(*Functions*)
lambda :: "(i => i) => i" (binder "lam " 10)
"`" :: "[i,i]=>i" (infixl 60)
@@ -58,6 +55,12 @@
(*Pairing*)
pair :: "[i,i]=>i" ("(1<_,/_>)")
+syntax
+ "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
+ "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
+ "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30)
+ "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50)
+
translations
"PROD x:A. B" => "Prod(A, %x. B)"
"A --> B" => "Prod(A, _K(B))"