"The problem is an alias rule can still fail if the syntax of the definition
doesn't meet certain criteria. [...]"
Maybe I should've been clearer about the syntax definition. In my theory, one
can skip a lot of parentheses since I considered left first bracketing, which I
explained prior to
On Wed, Jul 12, 2023 at 4:35 AM Marshall Stoner
wrote:
> I trust that intuitively that these definitions are valid. The problem is
> an alias rule can still fail if the syntax of the definition doesn't meet
> certain criteria. If the parenthesis surrounding ↔ were missing in the
> definition
I trust that intuitively that these definitions are valid. The problem is
an alias rule can still fail if the syntax of the definition doesn't meet
certain criteria. If the parenthesis surrounding ↔ were missing in the
definition of the biconditional, for instance. If I could understand how
Nevermind. I split the file into parts and found it easier that way.
On Monday, July 10, 2023 at 1:50:44 AM UTC-4 Marshall Stoner wrote:
> I just downloaded the metamath.exe program. It seems like this should be
> super obvious, but I just can't figure it out. The help documentation only
>
