Dear all,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Since I'm not too sure about the internals of local contexts, would that
make sense in principle?
A related question: what is the difference between
Syntax_Phases.term_check and Syntax_Phases.term_check'? Why does the
latter expect a function returning an option but not the former?
And another one: assume we could do
consts FOO :: ... (<some syntax>)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{const_name foo}
*}
would the overloading only be active inside foo or would it also have
effects outside of this context (that are impossible to avoid due to
technical reasons)? Does it make sense at all to use the locally fixed
foo as a constant in the call to add_overloaded?
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
