Re: [isabelle] Sort constraint finite inconsistent with default type for type variable "'b"



On 12/19/2012 05:20 AM, Florian Haftmann wrote:
Hi Christian,

Am 17.12.2012 04:46, schrieb Christian Sternagel:
locale a =
     fixes a :: "'b set => 'a set"
   begin

Here, 'b gets sort »type«…

   lemma
     fixes A :: "('b::finite) set"
     shows "P (a A)"

so it can't appear at sort »finite« later on.  Maybe you meant
»'c::finite«!?

Cheers,
	Florian

Hi Florian,

thanks for your reply. If I try "'c::finite", I get a type error, since "a" expects arguments of type "'b set" and not "'c set"...

However, in this particular case there is an obvious solution which I overlooked initially. Namely,

  lemma
    assumes "finite A"
    shows "P (a A)"

cheers

chris





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