[CakeML-Dev] case expressions with set_grammar_ancestry

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Sun Oct 9 10:09:17 UTC 2016

If grammar ancestry is set with the set_grammar_ancestry function in a script file, then case expressions won’t pretty-print properly (they’ll print with the underlying constants, e.g., option_CASES 1 (\n. n + 1)). I’ll fix this in HOL soon, but if you encounter this, the workaround is straightforward: use 

  temp_overload_on(“case”, ``option_CASE``)

for ``option_CASE``, ``pair_CASE``, ``list_CASE`` etc. 

Note that there is no issue if an ancestor has used set_grammar_ancestry, but your current script file does not.


More information about the Developers mailing list