equal
deleted
inserted
replaced
5 Syntax extension (internal interface). |
5 Syntax extension (internal interface). |
6 *) |
6 *) |
7 |
7 |
8 signature SYN_EXT0 = |
8 signature SYN_EXT0 = |
9 sig |
9 sig |
|
10 val dddot_indexname: indexname |
|
11 val constrainC: string |
10 val typeT: typ |
12 val typeT: typ |
11 val constrainC: string |
|
12 val max_pri: int |
13 val max_pri: int |
13 end; |
14 end; |
14 |
15 |
15 signature SYN_EXT = |
16 signature SYN_EXT = |
16 sig |
17 sig |
74 struct |
75 struct |
75 |
76 |
76 |
77 |
77 (** misc definitions **) |
78 (** misc definitions **) |
78 |
79 |
|
80 val dddot_indexname = (Lexicon.binding "dddot", 0); |
|
81 val constrainC = "_constrain"; |
|
82 |
|
83 |
79 (* syntactic categories *) |
84 (* syntactic categories *) |
80 |
85 |
81 val logic = "logic"; |
86 val logic = "logic"; |
82 val logicT = Type (logic, []); |
87 val logicT = Type (logic, []); |
83 |
88 |
89 val sprop = "#prop"; |
94 val sprop = "#prop"; |
90 val spropT = Type (sprop, []); |
95 val spropT = Type (sprop, []); |
91 |
96 |
92 val any = "any"; |
97 val any = "any"; |
93 val anyT = Type (any, []); |
98 val anyT = Type (any, []); |
94 |
|
95 |
|
96 (* constants *) |
|
97 |
|
98 val constrainC = "_constrain"; |
|
99 |
99 |
100 |
100 |
101 |
101 |
102 (** datatype xprod **) |
102 (** datatype xprod **) |
103 |
103 |