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
Thanks for the hint!
I'll try to use that then. However, the main goal was to use PolyML's
native log2 function anyway, which is likely much faster than anything
we can implement in Isabelle.
Manuel
On 2017-06-29 20:12, Thiemann, Rene wrote:
> Hi Manual,
>
> thanks for your efforts, but I
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.
13 matches
Mail list logo