On Tue, 24 Sep 2019 19:17:58 -0400, Mario Carneiro <[email protected]> wrote: > I think that this incident has made it clearer that we need a proper spec > for definition checking though, as well as at least one other > implementation, suitable as a reference implementation and not tied to a > complex system.
I agree, and I don't feel confident about creating such a definition myself. Someone :-) seems to have implemented a definition check in mmj2, current version here: https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js I think we should try to formalize what that is doing. Note that the recommended way to run this check is the following (which excludes axioms & some specific definitions): RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel Thoughts? --- David A. Wheeler -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iDIF6-0001cR-5u%40rmmprod07.runbox.
