35 val typ = Simple_Syntax.read_typ; |
35 val typ = Simple_Syntax.read_typ; |
36 |
36 |
37 val add_syntax = |
37 val add_syntax = |
38 Sign.root_path |
38 Sign.root_path |
39 #> Sign.add_types_global |
39 #> Sign.add_types_global |
40 [(Binding.make ("Type", @{here}), 0, NoSyn), |
40 [(Binding.make ("Type", \<^here>), 0, NoSyn), |
41 (Binding.make ("Null", @{here}), 0, NoSyn)] |
41 (Binding.make ("Null", \<^here>), 0, NoSyn)] |
42 #> Sign.add_consts |
42 #> Sign.add_consts |
43 [(Binding.make ("typeof", @{here}), typ "'b => Type", NoSyn), |
43 [(Binding.make ("typeof", \<^here>), typ "'b => Type", NoSyn), |
44 (Binding.make ("Type", @{here}), typ "'a itself => Type", NoSyn), |
44 (Binding.make ("Type", \<^here>), typ "'a itself => Type", NoSyn), |
45 (Binding.make ("Null", @{here}), typ "Null", NoSyn), |
45 (Binding.make ("Null", \<^here>), typ "Null", NoSyn), |
46 (Binding.make ("realizes", @{here}), typ "'a => 'b => 'b", NoSyn)]; |
46 (Binding.make ("realizes", \<^here>), typ "'a => 'b => 'b", NoSyn)]; |
47 |
47 |
48 val nullT = Type ("Null", []); |
48 val nullT = Type ("Null", []); |
49 val nullt = Const ("Null", nullT); |
49 val nullt = Const ("Null", nullT); |
50 |
50 |
51 fun mk_typ T = |
51 fun mk_typ T = |