Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Retrieve overloadings of constant

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Manuel Eberl <eberlm@in.tum.de>
Hello,

is there any way to retrieve the list of all overloaded definitions of a
given constant?

In particular, I'd like to find out if

  1. a given constant is overloaded or not
  2. if yes, what the list of types for which it has been overloaded is

It seems to me that this information is stored in the context (cf. e.g.
"get_overloading" in "overloading.ML"), but it does not seem to be
exposed to the outside.

Is there a deeper reason for this?

Manuel

view this post on Zulip Email Gateway (Aug 23 2022 at 09:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,

as long as you only refer to disciplined overloading, the data you are
searching for is in axclass.ML:
signature.asc

Last updated: Apr 26 2024 at 20:16 UTC