florian.haftmann at informatik.tu-muenchen.de
Wed Jun 16 13:16:53 CEST 2021
"global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
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
Both generalizations emerged by appropriate generalization of the
existing local theory stack with minimal effort.
This refers to adb34395b622
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev