equal
deleted
inserted
replaced
34 |
34 |
35 |
35 |
36 (** record **) |
36 (** record **) |
37 |
37 |
38 val record_decl = |
38 val record_decl = |
39 name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" -- |
39 (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "=" |
40 repeat1 ((name --$$ "::" -- typ) >> mk_pair) |
40 -- optional (typ --$$ "+" >> cat "Some") "None" |
|
41 -- repeat1 ((name --$$ "::" -- typ) >> mk_pair) |
41 >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
42 >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
42 |
43 |
43 |
44 |
44 (** (co)inductive **) |
45 (** (co)inductive **) |
45 |
46 |