> I think it would be beneficial for the Metamath community to have such a
tool, too. I've been thinking about it for a while.
Thierry, I've been also thinking that Metamath could benefit from some
collaboration, but I came to the conclusion that currently Metamath
community is probably too
The issue is that the '. syntax is ambiguous, A = B '. can be interpreted
as either "A = (B '.)" or "(A = B) '." . Syntax ambiguity in set.mm (and
most metamath databases) is a big no-no, you can generally prove a
contradiction from them, but because mmj2 parses formulas into trees
ambiguous
Thank you for the quick, and disappointing (as expected) answers.
The problematic definition:
$( Define Tick, Predicate ` ph '. <-> ( ph ^. 1 ) ` $)
df-bl.tick $a |- ( ph '. <-> ( ph ^. 1 ) ) $.
Because tick is used as syntactic sugar, I can do without it.
Unfortunately, I have other theorems
That error message means that the theorem df-bl.tick has a statement that
does not match the expression |- ( A = B '. <-> ( A = B ^. 1 ) ) that you
have provided. It's difficult to say more without seeing the rest of the
code (and in particular, the definition of `df-bl.tick`).
Q1: No, this is a
