1open HolKernel Parse boolLib
2
3open gh294aTheory gh294bTheory testutils
4
5val _ = new_theory "gh168b";
6
7val _ = remove_type_abbrev "foo"
8
9val tyg = type_grammar()
10
11val _ = tprint "foo abbrev no longer parses"
12val _ = (``:foo``; die "FAILED!") handle HOL_ERR _ => OK()
13
14fun typrinttest s =
15  let
16    val ty = Parse.Type [QUOTE s]
17  in
18    tprint (standard_tpp_message s);
19    if s = type_to_string ty then OK() else die "FAILED!"
20  end
21
22val _ = typrinttest ":bool -> bool"
23val _ = typrinttest ":bool -> bool -> bool"
24val _ = tprint "type_grammar abbrevs map is empty"
25val _ = if Binarymap.numItems (type_grammar.parse_map tyg) = 4 then OK()
26        else die "FAILED!"
27
28val _ = export_theory();
29