Email Gateway (Aug 19 2022 at 09:30): Email Gateway (Aug 19 2022 at 09:30):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 09:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 19 2022 at 09:34):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Last updated: May 06 2024 at 08:19 UTC