On 2/6/22 11:47, Mario Carneiro wrote:
Two things: (1) it's been done, see hol.mm <http://hol.mm> or dtt.mm <http://dtt.mm>.
At least in my email cilent these got linked funny. The references are to http://us.metamath.org/holuni/mmhol.html and https://github.com/digama0/dtt.mm respectively, as far as I know. Hope that helps people follow along in case anyone is unfamiliar.
-- 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/1f559443-b9ac-4175-485c-f9663c816abc%40panix.com.
