Re: Concatenation of finite sequences
Piotr Rudnicki <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
On Wed, Jan 12, 2011 at 3:57 AM, Freek Wiedijk <[email protected]> wrote: > ... > > 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. > I do not see the point of the permissive definition with 'assume'. Each time when using the operation I would have to state the assumption as a condition. We get the same effect without the inconvenience of permissiveness. PR -- Piotr Rudnicki http://www.cs.ualberta.ca/~piotr <http://www.cs.ualberta.ca/%7Epiotr>