Re: [mizar] Concatenation of finite sequences

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

Hi Piotr,

>I do not see the point of the permissive definition with
>'assume'.

It's similar to the author having to prove non-emptiness of
their types.  That's a big hassle, it doesn't serve a real
purpose either, but it forces the authors to think about what
they are doing so you get "better" formalizations.  I guess.

No, I wasn't fully serious about this permissive definition.

But _I_ don't see the point of having this operation only
"one way around".  It's very dual, so both definitions
should be there.

And I still think that the "don't remove either of the
endpoints if they differ" operation is the one you should
encourage people to use :-)

>Each time when using the operation I would have to state
>the assumption  as a condition.

Only when using the _definition_ of the operation, I guess?

Freek