OK, I'll turn it into a warning. If in the future we determine that it has
a legitimate use, we can easily turn off the warning. But the warning will
at least notify the user that something very unusual is being done.
Norm
On Saturday, April 18, 2020 at 10:47:30 AM UTC-4, savask wrote:
>
> I
I see, thank you for the answer. For a moment I thought that it's some sort
of arcane requirement I missed while reading the Metamath book :-)
Perhaps I should remove this error message.
>
It will be interesting to see comments from other people (and to see if
there are any malicious ways to
