[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds
bulwahn at in.tum.de
Mon Oct 22 08:22:12 CEST 2012
On 10/19/2012 04:35 PM, Makarius wrote:
> On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
>>> Operations like Simplifier.context, Simplifier.inherit_context
>>> should help here. Once that is repaired, I will see if the warning
>>> can now be made an error that is more explicit about the reasons.
>> I am certainly in favour of this. First, tool developers mainly react
>> on errors with test runs, but do not see the warnings. Secondly,
>> users do not know who to report those warnings and do not know if
>> they are caused by their scripts or the tools.
> Historically, the weak warning was a necessity due to too many
> simprocs still not working with the context.
> Let's hope that it can be easily switched to an explicit error after
> so many years now.
On the weekend, I had a look at this issue in the
set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and
already noticed what could make things difficult turning this into an error.
- the hypsubst_tac internally uses the simplifier, but the interface
does not allow to pass the current simpset to this tactic.
- An implementer has to avoid certain functions, such
asRaw_Simplifier.rewrite, that assume to be used only in a non-nested
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev