src/CTT/CTT.thy
changeset 22808 a7daa74e2980
parent 21524 7843e2fd14a9
child 23467 d1b97708d5eb
equal deleted inserted replaced
22807:715d01b34abb 22808:a7daa74e2980
    35   snd       :: "i=>i"
    35   snd       :: "i=>i"
    36   split     :: "[i, [i,i]=>i] =>i"
    36   split     :: "[i, [i,i]=>i] =>i"
    37   (*General Product and Function Space*)
    37   (*General Product and Function Space*)
    38   Prod      :: "[t, i=>t]=>t"
    38   Prod      :: "[t, i=>t]=>t"
    39   (*Types*)
    39   (*Types*)
    40   "+"       :: "[t,t]=>t"           (infixr 40)
    40   Plus      :: "[t,t]=>t"           (infixr "+" 40)
    41   (*Equality type*)
    41   (*Equality type*)
    42   Eq        :: "[t,i,i]=>t"
    42   Eq        :: "[t,i,i]=>t"
    43   eq        :: "i"
    43   eq        :: "i"
    44   (*Judgements*)
    44   (*Judgements*)
    45   Type      :: "t => prop"          ("(_ type)" [10] 5)
    45   Type      :: "t => prop"          ("(_ type)" [10] 5)
    49   Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
    49   Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
    50   (*Types*)
    50   (*Types*)
    51 
    51 
    52   (*Functions*)
    52   (*Functions*)
    53   lambda    :: "(i => i) => i"      (binder "lam " 10)
    53   lambda    :: "(i => i) => i"      (binder "lam " 10)
    54   "`"       :: "[i,i]=>i"           (infixl 60)
    54   app       :: "[i,i]=>i"           (infixl "`" 60)
    55   (*Natural numbers*)
    55   (*Natural numbers*)
    56   "0"       :: "i"                  ("0")
    56   "0"       :: "i"                  ("0")
    57   (*Pairing*)
    57   (*Pairing*)
    58   pair      :: "[i,i]=>i"           ("(1<_,/_>)")
    58   pair      :: "[i,i]=>i"           ("(1<_,/_>)")
    59 
    59