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?
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" *)
> lemma pred_is_UNIV: "pred A B"
> by (metis a1)
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and