On Sunday, December 22, 2019 at 4:34:17 PM UTC+1, Mario Carneiro wrote: > > ... set.mm would have been an optimal starting point, except it's HUGE, > which makes introductory stuff harder. Even worse, it starts with a comment > that is tens of thousands of lines long, which makes it very difficult to > see how "baby's first propositional logic" is supposed to go. > Maybe a first step to purify set.mm could be to extract the "history" in section "1. Recent label changes" at the beginning of set.mm into a separate file - this would save (currently) about 10.000 lines ...
-- 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/dd224ef4-03cf-4d3e-9a56-e5e19d644672%40googlegroups.com.
