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
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
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