1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "mdt";
4
5val _ = new_type ("char", 0)
6
7val _ = type_abbrev_pp("string", ``:char list``)
8
9val _ = Hol_datatype`
10  term = Var of string => type
11       | Const of string => type => const_tag
12       | Comb of term => term
13       | Abs of string => type => term
14       ;
15   type = Tyvar of string
16       | Tyapp of type_op => type list
17       ;
18   type_op =
19     Typrim of string => num
20   | Tydefined of string => term
21       ;
22   const_tag =
23     Prim
24   | Defined of num => (string # term) list => term
25   | Tyabs of string => term
26   | Tyrep of string => term
27`;
28
29val _ = Datatype`testrcd = <| fld1 : bool ; fld2 : 'a -> num |>`;
30
31val _ = export_theory();
32