Stream: Isabelle/ML

Topic: Instantiation get instantiated type

view this post on Zulip Jonas Stahl (Aug 09 2024 at 15:27):

Hi everyone,
I'm inside of an instantiation as here:

instantiation list :: (_) T_size
begin

Is there a way to get the instantiated type (here: list), probably out of the context?

view this post on Zulip Kevin Kappelmann (Aug 13 2024 at 09:32):

Maybe something in the ML structure Class (haven't tried it myself).

Last updated: Jan 08 2026 at 16:33 UTC