Hi, Il 25/09/19 01:17, Mario Carneiro ha scritto: > 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. Unfortunately definition checking requires higher > parsing requirements than verification, because axioms don't come with > parse trees, plus you have to be able to read $j rules (or be willing to > hardcode lots of things like the names of sorts).
mmpp more or less has these capabilities, and I have though about reimplementing the definition checker in the past, but never did it. This could be an occasion to resume that project. It should not be hard. In case there isn't one already, though, I would need a specification of what has to be checked. I have a fairly good idea of what it is, but I might be mistaken, and comparing with an external reference definition is always good in these cases. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/794b6998-8d7c-4325-a641-e9e562d26cc7%40gmail.com.
signature.asc
Description: OpenPGP digital signature
