[isabelle] adhoc_overloading removes type constraints
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] adhoc_overloading removes type constraints
- From: Dominique Unruh <unruh at ut.ee>
- Date: Sun, 19 May 2019 22:47:59 +0300
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1
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.)
consts someop :: "'a list ⇒ 'a list"
consts overload :: "'a ⇒ 'b"
adhoc_overloading overload someop
term "overload  :: bool list"
:: "'a list"
By the way, I would like to check whether this mailing list is the right
place for sharing this kind of reports.
This archive was generated by a fusion of
Pipermail (Mailman edition) and