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? Tobias
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 isIncidentally, 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. LarryOn 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
