Re: [isabelle] Apply rule: unexpected behaviour



Hi Lars,

The clash information I get is this: "Lattices.sup_class.sup =/=
Set.insert".

It understood that it has to do with the usage of sets, but I will need to
find out
how this message can help me. Does this clash message ring a bell for you?


Thanks for you help!
Diego


On 13 March 2016 at 18:59, Lars Hupel <hupel at in.tum.de> wrote:

> Hi Diego,
>
> > Is there any way of extracting more information from Isabelle about the
> > reason that causes the application of a rule to fail?
>
> try this:
>
>   using [[unify_trace_failure]]
>   apply (rule ...)
>
> Then, you'll find the output like the following:
>
>   Clash: Scratch.P =/= Scratch.Q
>
> Hope that helps.
>
> Cheers
> Lars
>



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