Re: [isabelle] Retrieve overloadings of constant



Hi Manuel,

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

>   val class_of_param: theory -> string -> class option
>   val instance_name: string * class -> string
>   val param_of_inst: theory -> string * string -> string
>   val inst_of_param: theory -> string -> (string * string) option
>   val unoverload: Proof.context -> thm -> thm
>   val overload: Proof.context -> thm -> thm
>   val unoverload_conv: Proof.context -> conv
>   val overload_conv: Proof.context -> conv
>   val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
>   val unoverload_const: theory -> string * typ -> string

overloading.ML manages the overloading target(s), not the logical
concept of overloading.

If you also have to cover undisciplined overloading, go one step further
down to defs.ML.

Hope this helps,
	Florian

Am 29.05.20 um 18:30 schrieb Manuel Eberl:
> 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
> 

Attachment: signature.asc
Description: OpenPGP digital signature



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