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



Hi all,

in the lemma of the following (minimal) example I get:

Sort constraint finite inconsistent with default type for type variable "'b"

  locale a =
    fixes a :: "'b set => 'a set"
  begin

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

Is this an inherent limitation?

cheers

chris





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