equal
deleted
inserted
replaced
13 open Datatype_Aux (* typ_of_dtyp, DtRec, ... *); |
13 open Datatype_Aux (* typ_of_dtyp, DtRec, ... *); |
14 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}) |
14 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}) |
15 *} |
15 *} |
16 |
16 |
17 ML {* dest_Type @{typ rlam} *} |
17 ML {* dest_Type @{typ rlam} *} |
|
18 |
|
19 (* Bindings are given as a list which has a length being equal |
|
20 to the length of the number of constructors. Each element |
|
21 is a specification of all the bindings n this constructor. |
|
22 The bindings are given as triples: function, bound argument, |
|
23 and the argument in which it is bound. |
|
24 |
|
25 Eg: |
|
26 nominal_datatype |
|
27 |
|
28 C1 |
|
29 | C2 x y z bind x in z |
|
30 | C3 x y z bind f x in y bind g y in z |
|
31 |
|
32 yields: |
|
33 [[], [(NONE, 0, 2)], [(SOME (Const f), 0, 1), (Some (Const g), 1, 2)]] |
|
34 *) |
18 |
35 |
19 ML {* |
36 ML {* |
20 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
37 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
21 val sorts = []; |
38 val sorts = []; |
22 |
39 |