1open HolKernel Parse boolLib Datatype
2
3val _ = new_theory "gh224a";
4
5(* val _ = Datatype `bar = <| size : num |>` *)
6
7val _ = Datatype `A_x = <| y : num |>`
8val _ = Datatype `A = <| x : A_x |>`
9
10
11val _ = export_theory();
12