src/CCL/type.thy
changeset 22 41dc6b189412
parent 0 a5a9c433f639
equal deleted inserted replaced
21:b5f8677e24e7 22:41dc6b189412
    33   "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
    33   "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
    34   "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
    34   "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
    35 
    35 
    36 translations
    36 translations
    37   "PROD x:A. B" => "Pi(A, %x. B)"
    37   "PROD x:A. B" => "Pi(A, %x. B)"
       
    38   "A -> B"      => "Pi(A, _K(B))"
    38   "SUM x:A. B"  => "Sigma(A, %x. B)"
    39   "SUM x:A. B"  => "Sigma(A, %x. B)"
       
    40   "A * B"       => "Sigma(A, _K(B))"
    39   "{x: A. B}"   == "Subtype(A, %x. B)"
    41   "{x: A. B}"   == "Subtype(A, %x. B)"
    40 
    42 
    41 rules
    43 rules
    42 
    44 
    43   Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
    45   Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
    61 end
    63 end
    62 
    64 
    63 
    65 
    64 ML
    66 ML
    65 
    67 
    66 val parse_translation =
       
    67   [("@->", ndependent_tr "Pi"),
       
    68    ("@*", ndependent_tr "Sigma")];
       
    69 
       
    70 val print_translation =
    68 val print_translation =
    71   [("Pi", dependent_tr' ("@Pi", "@->")),
    69   [("Pi", dependent_tr' ("@Pi", "@->")),
    72    ("Sigma", dependent_tr' ("@Sigma", "@*"))];
    70    ("Sigma", dependent_tr' ("@Sigma", "@*"))];
    73 
    71