Another possibility is to call one of them is_subseq.


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?


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.

If anybody has better suggestions, I am open to implementing them.


On 2017-06-28 17:05, Andreas Lochbihler wrote:
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 subsequence. This name is now hidden by the definition in
Sublist, in particular when I import HOL-Probability.

Can this name clash be eliminated before the next release such that I
don't have to write Topological_Spaces.subseq everywhere?


On 26/05/17 08:16, Tobias Nipkow wrote:
Thank you for your research. I am perfectly happy with "sublist" (for
the contiguous case) and "subseq" (for the general case) and think we
should adopt it.

[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
nat set ⇒ 'a list" (in List) to something else, eg sublist_index)


On 25/05/2017 21:13, Jasmin Blanchette wrote:

On 25.05.2017, at 20:41, Tobias Nipkow <> wrote:

I don't think that sublist, subsequence and substring really have
much of a bias in either direction, except possibly substring, but
the latter does indeed sound too specialized.

Wikipedia has a clear bias (and I did not edit it, nor did I look it
up before writing my previous email):

Popular algorithm sbooks like Cormen et al. follow the same
definition of subsequence. Standard expressions like "longest
increasing subsequence" depend on this semantics.

As for sublist, all the examples I see by Googling either "sublist",
"is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
Scala, etc., have the contiguous semantics. Including this page:

I'm not saying we should rename the Isabelle concepts, just that
Isabelle is the odd (wo)man out.


isabelle-dev mailing list
isabelle-dev mailing list

isabelle-dev mailing list

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to