[isabelle-dev] [isabelle] Good name for "sublist" predicates
nipkow at in.tum.de
Fri Jun 30 16:52:17 CEST 2017
On 30/06/2017 16:39, Manuel Eberl wrote:
> I do understand that argument, but I am not sure if Topological_Spaces.subseq is
> really used /that/ often. Actually, going one step further, it is nothing more
> than "strict_mono" restricted to "nat ⇒ nat", so one may well argue that it is
> superfluous anyway.
If we can get rid of it all together, surely that is the best option?
> The possibility of renaming one of them to "subsequence" or "is_subseq" is, in
> my opinion, not a satisfactory solution, since we would then /still/ have two
> completely different constants with essentially the same name, just with an
> arbitrary artificial difference. We might as well call one of them subseq'.
> The advantage of qualified names is that they really allow us to add
> disambiguating context to ambiguous names when necessary, e.g. something like
> "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I do understand
> that typing such lengthy names is tedious.
> I currently see the following possible solutions:
> – find another good name for one of the two things currently named "subseq" and
> rename it
> – introduce an arbitrary distinction like "subsequence" or "is_subseq"
> – move "subseq" to List.thy and make it qualified, so that one must write
> – remove Topological_Spaces.subseq entirely, replacing it by strict_mono
> – leave everything as it is
> Incidentally, I wonder if it is possible to locally prefer one of the two
> constants, i.e. say that, in the following block, I want "subseq" to mean
> "Topological_Spaces.subseq". That might also mitigate the problem of long
> qualified names.
> On 2017-06-30 16:23, Tobias Nipkow wrote:
>> In theory that solves the problem, but the point is that
>> Topological_Spaces.subseq is impractical for a frequently used symbol. It
>> would be nice if non-quaified names could be found for this case.
>> On 30/06/2017 16:14, Lawrence Paulson wrote:
>>> Indeed we do.
>>>> On 28 Jun 2017, at 18:49, Manuel Eberl <eberlm at in.tum.de
>>>> <mailto:eberlm at in.tum.de>> wrote:
>>>> Yes, I noticed that as well. I decided to leave it that way since, well,
>>>> we do have qualified names.
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev