src/CTT/CTT.thy
changeset 14765 bafb24c150c1
parent 14565 c6dc17aab88a
child 14854 61bdf2ae4dc5
     1.1 --- a/src/CTT/CTT.thy	Wed May 19 11:41:58 2004 +0200
     1.2 +++ b/src/CTT/CTT.thy	Fri May 21 21:14:18 2004 +0200
     1.3 @@ -34,6 +34,8 @@
     1.4    split     :: "[i, [i,i]=>i] =>i"
     1.5    (*General Product and Function Space*)
     1.6    Prod      :: "[t, i=>t]=>t"
     1.7 +  (*Types*)
     1.8 +  "+"       :: "[t,t]=>t"           (infixr 40)
     1.9    (*Equality type*)
    1.10    Eq        :: "[t,i,i]=>t"
    1.11    eq        :: "i"
    1.12 @@ -44,12 +46,7 @@
    1.13    Eqelem    :: "[i,i,t]=>prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)
    1.14    Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
    1.15    (*Types*)
    1.16 -  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    1.17 -  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    1.18 -  "+"       :: "[t,t]=>t"           (infixr 40)
    1.19 -  (*Invisible infixes!*)
    1.20 -  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    1.21 -  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
    1.22 +
    1.23    (*Functions*)
    1.24    lambda    :: "(i => i) => i"      (binder "lam " 10)
    1.25    "`"       :: "[i,i]=>i"           (infixl 60)
    1.26 @@ -58,6 +55,12 @@
    1.27    (*Pairing*)
    1.28    pair      :: "[i,i]=>i"           ("(1<_,/_>)")
    1.29  
    1.30 +syntax
    1.31 +  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    1.32 +  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    1.33 +  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    1.34 +  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
    1.35 +
    1.36  translations
    1.37    "PROD x:A. B" => "Prod(A, %x. B)"
    1.38    "A --> B"     => "Prod(A, _K(B))"