Re: Concatenation of finite sequences
Freek Wiedijk <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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