"global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
"global_interpretation".
Using "global_interpretation" in instantiation targets provides a direct
way to transfer logical relations in the module system to type class
instances and can emulate the concept of default type class instances
from Haskell. An example can be found in theory HOL-Library.Saturated.
Using "global_interpretation" in nested targets provides a way to
express the idea of »conditional interpretation« where the
interpretation depends on additional predicates which turn into explicit
assumptions after interpretation. A minimal example can be found in
theory HOL-ex.Interpretation_in_nested_targets.
Both generalizations emerged by appropriate generalization of the
existing local theory stack with minimal effort.
This refers to adb34395b622
Florian
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
