[CakeML-dev] Translation failure

Scott Owens S.A.Owens at kent.ac.uk
Sat Apr 8 16:12:29 UTC 2017

I’m seeing the translator fail on a pretty simple function that coverts inferencer types to strings in inferProgScript.sml on the type-error-loc branch. The error message is unhelpful.

Improved induction theorem: inf_type_to_string_ind
Failed translation: inf_type_to_string, inf_types_to_string
Exception- HOL_ERR {message = "not an \"=\"", origin_function = "dest_eq(_ty)", origin_structure = "boolSyntax"} raised

Does anyone have any ideas what the problem might be, or tips on debugging translator failures?


More information about the Developers mailing list