Email Gateway (Aug 22 2022 at 19:54): Email Gateway (Aug 22 2022 at 19:54):From: Dominique Unruh <unruh@ut.ee>
Hi,
in the following theory, the term "overload [] :: bool list" is parsed
as "overload [] :: 'a list". It seems there is some accidental erasure
of the type constraint in the adhoc overloading mechanism.
(Tested with 2018 and 2019-RC0, so it's not a regression.)
theory Scratch
imports "HOL-Library.Adhoc_Overloading"
begin
consts someop :: "'a list ⇒ 'a list"
consts overload :: "'a ⇒ 'b"
adhoc_overloading overload someop
term "overload [] :: bool list"
(* Prints:
"overload []"
:: "'a list"
*)
By the way, I would like to check whether this mailing list is the right
place for sharing this kind of reports.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:54):From: Alexander Krauss <krauss@in.tum.de>
Hi Dominique,
Am 19.05.2019 um 21:47 schrieb Dominique Unruh:
in the following theory, the term "overload [] :: bool list" is parsed
as "overload [] :: 'a list". It seems there is some accidental erasure
of the type constraint in the adhoc overloading mechanism.
Thanks for reporting this. I can see where Adhoc_Overloading discards
the type information here. I'll see if I can fix this.
By the way, I would like to check whether this mailing list is the right
place for sharing this kind of reports.
Absolutely.
Alex
Last updated: Apr 26 2024 at 20:16 UTC