<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">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.</font></p>
<p><font size="+1">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'.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">I currently see the following possible solutions:</font></p>
<font size="+1">– find another good name for one of the two things
currently named "subseq" and rename it<br>
– introduce an arbitrary distinction like "subsequence" or
"is_subseq"<br>
– move "subseq" to List.thy and make it qualified, so that one
must write "List.subseq"<br>
– remove Topological_Spaces.subseq entirely, replacing it by
strict_mono<br>
– leave everything as it is<br>
</font>
<p><font size="+1">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.<br>
</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<br>
<div class="moz-cite-prefix">On 2017-06-30 16:23, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:ffd2281d-bfa6-3867-98da-764832c0f1c6@in.tum.de">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.
<br>
<br>
Tobias
<br>
<br>
On 30/06/2017 16:14, Lawrence Paulson wrote:
<br>
<blockquote type="cite">Indeed we do.
<br>
Larry
<br>
<br>
<blockquote type="cite">On 28 Jun 2017, at 18:49, Manuel Eberl
<<a class="moz-txt-link-abbreviated" href="mailto:eberlm@in.tum.de">eberlm@in.tum.de</a> <a class="moz-txt-link-rfc2396E" href="mailto:eberlm@in.tum.de"><mailto:eberlm@in.tum.de></a>>
wrote:
<br>
<br>
Yes, I noticed that as well. I decided to leave it that way
since, well,
<br>
we do have qualified names.
<br>
</blockquote>
<br>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>