Re: [isabelle] Variables in locale assumptions



The error seems sensible to me. In a1, R is a relation, and in a2 it's a set. Or maybe I'm missing something?

John

On 21 Feb 2014, at 16:13, Van Staden Stephan <stephan.vanstaden at inf.ethz.ch> wrote:

> Dear all,
> 
> In Isabelle/jEdit 2013-2, the following locale works fine:
> 
> locale Test =
>  fixes pred :: "'a set ⇒ 'a rel ⇒ bool"
>  assumes a1: "pred S R"
> (*  assumes a2: "pred R S" *)
> begin
> lemma pred_is_UNIV: "pred A B"
>  by (metis a1)
> end
> 
> However, uncommenting assumption a2 gives me the following error:
> 
> Type unification failed
> Type error in application: incompatible operand type
> Operator:  pred :: 'a set ⇒ ('a × 'a) set ⇒ bool
> Operand:   R :: ('a × 'a) set
> 
> Page 2 of the locale tutorial seems to suggest that this is a bug. Or should I expect this behaviour?
> 
> Thanks in advance!
> Stephan
> 





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