On Wed, Jan 12, 2011 at 3:57 AM, Freek Wiedijk
<freek@cs.ru.nl> 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