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 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 use this peculiarity), but in case it all > works out well, may I suggest to modify the metamath program in a way such > that these kinds of proofs would check, but the program would still show a > warning message? That way we may eventually find out if there's any use to > this behavior. > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/32649501-1a5a-4d72-8705-126a500067d4%40googlegroups.com.
