Post #2479118

@MartinEscardo@mathstodon.xyz I'm not sure there is anything about error reporting and/or recovery which inherently makes an implementation slow, but for what it is worth I typically use two implementations of the metamath proof verifier. One is fast, and the other gives better error messages (particularly in one commonly encountered situation). As far as I know this is an accident of history and the error messages I'm looking for may eventually get added to the fast verifier. @olynch@mathstodon.xyz