Re: [isabelle] How tactic fold instantiates variables
I donât have anything to explain about the code, other than to note that the comments refer to critical pairs. This is a reminder that a set of rewrite rules can be ambiguous. Instantiating variables is one way to cope with ambiguity, and it also helps if folding the right hand side would involve higher-order matching.
> On 23 Jun 2015, at 22:17, Makarius <makarius at sketis.net> wrote:
> (This old thread still looks unsettled.)
> On Fri, 29 May 2015, Daniel Raggi wrote:
>> When folding a definition, why would someone (in some cases), need to
>> specify instantiations of variables using [where "X = ..."]?
>> I can see how it's useful to do it in some cases to avoid having to
> First note that (fold eq) is the same as (unfold eq [symmetric]).
> For more than one equation, there is a slight difference in the initial order, although the details are unclear to me; see src/Pure/raw_simplifer.ML:
> val rev_defs = sort_lhs_depths o map Thm.symmetric;
> Larry might be able to explain that code "from the depths of time", as he usually says; see
This archive was generated by a fusion of
Pipermail (Mailman edition) and