Re: [isabelle] of/where with dummy-patterns
On Fri, 26 Jun 2015, Peter Lammich wrote:
more or less intuitively, I used the of-attribute with dummy-patterns,
thm imp_refl[of "undefined _ _"]
inside a proof, this works fine. However, outside a proof, I get the
Duplicate fixed variable(s): "uu_"
The same behaviour for "where".
Is the of-attribute supposed to work with dummy-patterns or
do they only work by accident within proofs?
It is official since Isabelle2015, see NEWS:
* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.
The breakdown above indicates that I've got the context policy wrong for
the "eigen context" of dummy variables. I need to revisit the whole
complex again for the next release anyway: the main point is to have
instantiations work properly in Eisbach, and we are only half-way through
Right now it works outside a proof body for at most one dummy variable. In
any case the result will be a bit ugly: some derivative of "uu".
This archive was generated by a fusion of
Pipermail (Mailman edition) and