1open HolKernel Parse boolLib bossLib; 2 3val _ = new_theory "mdt"; 4 5val _ = new_type ("char", 0) 6 7val _ = type_abbrev("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