Re: [isabelle] Question on sequential pattern matching



The real case has two different datatypes as arguments to f, additional conditions on constructor arguments, etc. I’ve reduced it to what may be a minimal example. The issue doesn’t arise with just two constructors.



On Dec 30, 2013, at 1:27 AM, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:

> 
> I don't know how close is the artificial case to the real case, still what about this one:
> 
>    fun f :: "T ⇒ T ⇒ bool"
>      where "f x y ⟷ x = y"
> 
> Then…
> 
>    thm f.simps
> 
> …just says:
> 
>    f ?x ?y = (?x = ?y)

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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