src/Cube/Cube.thy
changeset 21 b5f8677e24e7
parent 0 a5a9c433f639
child 351 1718ce07a584
equal deleted inserted replaced
20:e6fb60365db9 21:b5f8677e24e7
    23   ""            :: "var => context"                     ("_ ")
    23   ""            :: "var => context"                     ("_ ")
    24   Context       :: "[typing, context] => context"       ("_ _")
    24   Context       :: "[typing, context] => context"       ("_ _")
    25   star          :: "term"                               ("*")
    25   star          :: "term"                               ("*")
    26   box           :: "term"                               ("[]")
    26   box           :: "term"                               ("[]")
    27   "^"           :: "[term, term] => term"               (infixl 20)
    27   "^"           :: "[term, term] => term"               (infixl 20)
    28   Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
    28   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    29   Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
    29   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    30   "->"          :: "[term, term] => term"               (infixr 10)
    30   "->"          :: "[term, term] => term"               (infixr 10)
    31   Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    31   Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    32 
    32 
    33 translations
    33 translations
    34   (prop) "x:X"  == (prop) "|- x:X"
    34   (prop) "x:X"  == (prop) "|- x:X"
    35   "Lam x:A. B"  == "Abs(A, %x. B)"
    35   "Lam x:A. B"  == "Abs(A, %x. B)"
    36   "Pi x:A. B"   => "Prod(A, %x. B)"
    36   "Pi x:A. B"   => "Prod(A, %x. B)"
       
    37   "A -> B"      => "Prod(A, _K(B))"
    37 
    38 
    38 rules
    39 rules
    39   s_b           "*: []"
    40   s_b           "*: []"
    40 
    41 
    41   strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
    42   strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
    53 end
    54 end
    54 
    55 
    55 
    56 
    56 ML
    57 ML
    57 
    58 
    58 val parse_translation = [("op ->", ndependent_tr "Prod")];
       
    59 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    59 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    60 
    60