16 |
16 |
17 nonterminals |
17 nonterminals |
18 context' typing' |
18 context' typing' |
19 |
19 |
20 consts |
20 consts |
21 Abs :: "[term, term => term] => term" |
21 Abs :: "[term, term => term] => term" |
22 Prod :: "[term, term => term] => term" |
22 Prod :: "[term, term => term] => term" |
23 Trueprop :: "[context, typing] => prop" |
23 Trueprop :: "[context, typing] => prop" |
24 MT_context :: "context" |
24 MT_context :: "context" |
25 Context :: "[typing, context] => context" |
25 Context :: "[typing, context] => context" |
26 star :: "term" ("*") |
26 star :: "term" ("*") |
27 box :: "term" ("[]") |
27 box :: "term" ("[]") |
28 app :: "[term, term] => term" (infixl "^" 20) |
28 app :: "[term, term] => term" (infixl "^" 20) |
29 Has_type :: "[term, term] => typing" |
29 Has_type :: "[term, term] => typing" |
30 |
30 |
31 syntax |
31 syntax |
32 Trueprop :: "[context', typing'] => prop" ("(_/ |- _)") |
32 "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)") |
33 Trueprop1 :: "typing' => prop" ("(_)") |
33 "_Trueprop1" :: "typing' => prop" ("(_)") |
34 "" :: "id => context'" ("_") |
34 "" :: "id => context'" ("_") |
35 "" :: "var => context'" ("_") |
35 "" :: "var => context'" ("_") |
36 MT_context :: "context'" ("") |
36 "\<^const>Cube.MT_context" :: "context'" ("") |
37 Context :: "[typing', context'] => context'" ("_ _") |
37 "\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _") |
38 Has_type :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5) |
38 "\<^const>Cube.Has_type" :: "[term, term] => typing'" ("(_:/ _)" [0, 0] 5) |
39 Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) |
39 "_Lam" :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10) |
40 Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) |
40 "_Pi" :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10) |
41 arrow :: "[term, term] => term" (infixr "->" 10) |
41 "_arrow" :: "[term, term] => term" (infixr "->" 10) |
42 |
42 |
43 translations |
43 translations |
44 ("prop") "x:X" == ("prop") "|- x:X" |
44 ("prop") "x:X" == ("prop") "|- x:X" |
45 "Lam x:A. B" == "CONST Abs(A, %x. B)" |
45 "Lam x:A. B" == "CONST Abs(A, %x. B)" |
46 "Pi x:A. B" => "CONST Prod(A, %x. B)" |
46 "Pi x:A. B" => "CONST Prod(A, %x. B)" |
47 "A -> B" => "CONST Prod(A, %_. B)" |
47 "A -> B" => "CONST Prod(A, %_. B)" |
48 |
48 |
49 syntax (xsymbols) |
49 syntax (xsymbols) |
50 Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") |
50 "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \<turnstile> _)") |
51 box :: "term" ("\<box>") |
51 "\<^const>Cube.box" :: "term" ("\<box>") |
52 Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) |
52 "_Lam" :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10) |
53 Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
53 "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
54 arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10) |
54 "_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10) |
55 |
55 |
56 print_translation {* |
56 print_translation {* |
57 [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))] |
57 [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] |
58 *} |
58 *} |
59 |
59 |
60 axioms |
60 axioms |
61 s_b: "*: []" |
61 s_b: "*: []" |
62 |
62 |