Hi Igor, hi David, I think the current status of metamath-lamp is already very good, but not good enough for a beginner. So there is room for some improvements (especially regarding documentation, as indicated by David). In any case, it is a good candidate to replace the Metamath Solitaire Applet (does it actually work somewhere/somehow?) very soon. Maybe a restriction of the scope (for beginners) could help: if only propositional or predicate calculus (or ZF set theory) is used (this is a great functionality of methamath-lamp to restrict the amount of set.mm to be loaded and used. "Stop at exists2" would only load definitions and theorems for propositional or predicate calculus, "Stop at hsmex3" for ZF set theory), metamath-lamp may be fast and intuitive enough for a beginner.
-- 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/55c6fe42-129c-4742-a211-5dad3d9d3076n%40googlegroups.com.
