Re: [mizar] Concatenation of finite sequences

[Freek Wiedijk <freek@cs.ru.nl>]

Andrzej,

>In the interesting case (when they coincide) the result
>is the same.  So, to keep the integrity of MML we should
>remove one of the definitions.

Sorry, but I don't understand this.  These operations are
not the same?  So why remove one of them?

If you only want to apply them in the "interesting" case,
you should add an "assume" at the start of the definition
that states that the operation needs the last element of
the first argument to be equal to the first of the last.

In that case the question becomes: what notation is to
be preferred?

Or is the question which one you want to encourage the
authors of MML to use for this kind of concatenations?
But you _don't_ want the assumption because that is a pain?
Still, what does it matter which one of the two you choose
for that then?

Another operation is to do "normal" concatenation if the
two endpoints don't match.  So only remove the duplicate
one if it's actually duplicate.  That one has the nice
property that even without assumptions it distributes over
sequence reversal.  (Neither of the two that you give have
that property, right?)

Freek