Re: [isabelle] adhoc_overloading raises TYPE in locale when coercions are enabled

On Mon, 18 Nov 2013, Dmitriy Traytel wrote:

Now that I thought about it: since the coercion inference reports an error, I cannot guarantee that some subterm of the type-incorrect term is well-typed in general (so I barely can print anything, if printing requires well-typed terms). Hence, uncheck should better work with type-incorrect terms.

Syntax.uncheck_terms is indeed required to allow printing of bad terms, otherwise most error messages would be impossible to deliver. The burden here is on all user-space tools that add to that abstract syntax phase via Syntax_Phases.term_uncheck.

These are not everyday user applications, but user-space nonetheless -- analogous to simplification procedures written in Isabelle/ML.

The particular problem with adhoc_overloading is addressed in the next release (in about 1 week).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.