[isabelle-dev] Common Names
nipkow at in.tum.de
Fri May 30 18:31:12 CEST 2008
Dear theory developers,
From time to time I find that somebody has added some function to
HOL/Main that has a generic name (like `swap') but a fairly specific
meaning (like "swap a b f = f(a := f b, b := f a)").
The disadvantage: since the name is common, it is likely that others
have used it (or are going to), and they are suddenly confronted with
qualified names MyTheory.swap through no fault of their own. It is not a
disaster, but, for example, tends to mess up documentation produced by
Could I urge everybody to
1. Consider carefully if such constants really needs to go into Main.
2. If they do, please hide the name:
hide const swap
It is still available in qualified form,
but does not force new definitions of swap to be qualified.
What about uncommon names like `my_very_special_f'?
They should not be in Main to start with.
Thanks, and a wonderful summer w/e!
PS Am in the process of hiding swap.
More information about the isabelle-dev