On 30/06/17 16:39, Manuel Eberl wrote:
>
> 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
See now Isabelle/4c999b5d78e2.
Andreas
On 30/06/17 21:31, Tobias Nipkow wrote:
On 30/06/2017 20:41, Manuel Eberl wrote:
By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly
It's "Topological_Spaces.compact" and that
Hi all,
Yes, it absolutely makes sense to change the situation with compact. It is a standard
notion in order theory, so my suggestion is to make it qualified with ccpo, just like
admissible and fixp are. I can take care of that.
Andreas
On 30/06/17 21:31, Tobias Nipkow wrote:
On
Just for the record:
* Topological_Spaces.subseq has already been present before 2007 in
HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7)
* strict_mono has entered in 2009, see abefe1dfadbb
Hence we have the typical situation that a generalized constant subsumes
a more ancient unconsciously.
Cheers,
On 30/06/2017 20:41, Manuel Eberl wrote:
By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly
It's "Topological_Spaces.compact" and that should definitely work. We
should probably make the one from Complete_Partial_Order2
Le 30/06/2017 à 20:41, Manuel Eberl a écrit :
So what about the suggestion of just writing "strict_mono" instead?
Besides, you can always introduce local abbreviations for things with
"notation" and delete them with "no_notation" afterwards.
strict_mono would be perfectly OK if there is a
On 2017-06-30 20:33, Sebastien Gouezel wrote:
> I used subseq quite heavily in my ergodic theory developments. From
> a mathematician point of view, taking subsequences of sequences
> from nat to nat is very common and very useful in analysis (much
> more than taking subsequences of lists).
So
Le 30/06/2017 à 16:57, Manuel Eberl a écrit :
I agree about 90%, I think, but one could argue that "subseq" contains
additional meta-information: the semantic meaning is that it is a
strictly monotonic function, but the idea behind it is that it describes
a sub-sequence of some other sequence.
As I recall, this constant originally comes from HOL Light and is used in a
couple of proofs.
And it occurs to me that it might be a good way of dealing with HOL Light’s
generalisation of summations and limits to sets of natural numbers. As I ported
the PNT, I used two other methods of dealing
I agree about 90%, I think, but one could argue that "subseq" contains
additional meta-information: the semantic meaning is that it is a
strictly monotonic function, but the idea behind it is that it describes
a sub-sequence of some other sequence.
Still, I for one think this is not really worth
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
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
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
Indeed we do.
Larry
> On 28 Jun 2017, at 18:49, Manuel Eberl 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
Another possibility is to call one of them is_subseq.
Tobias
On 30/06/2017 08:17, Andreas Lochbihler wrote:
Hi Manuel,
Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly
strict_subseq to strict_subsequence or ssubsequence?
Andreas
On 28/06/17 19:49, Manuel
Hi Manuel,
Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly
strict_subseq to strict_subsequence or ssubsequence?
Andreas
On 28/06/17 19:49, Manuel Eberl wrote:
Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.
Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.
If anybody has better suggestions, I am open to implementing them.
Manuel
On 2017-06-28 17:05, Andreas Lochbihler wrote:
> Dear all,
>
> While porting some of my theories to the current
Dear all,
While porting some of my theories to the current development version, I've just noticed
that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad
effect:
The name subseq is already used in Topological_Spaces to formalise the concept of a
18 matches
Mail list logo