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.
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 "List.subseq" – 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. Manuel 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. > > Tobias > > On 30/06/2017 16:14, Lawrence Paulson wrote: >> Indeed we do. >> Larry >> >>> On 28 Jun 2017, at 18:49, Manuel Eberl <ebe...@in.tum.de >>> <mailto:ebe...@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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
