> On Oct 7, 2020, at 5:11 PM, Mario Carneiro <[email protected] > <mailto:[email protected]>> wrote: ...
> On Oct 7, 2020, at 5:25 PM, David A. Wheeler <[email protected]> wrote: > This is a nice answer. > > We do note this in: http://us.metamath.org/mpeuni/mmset.html#proofs > <http://us.metamath.org/mpeuni/mmset.html#proofs> under “legal syntax”. > However, it’s probably too abstract as it’s currently written. I plan to > tweak this question & answer as a proposed extension to the “legal syntax” > part, because this specific answer may make it much clearer. I tried to capture this discussion in this pull request: https://github.com/metamath/set.mm/pull/1843 <https://github.com/metamath/set.mm/pull/1843> -- 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/EF1ED7AC-55A0-499B-A104-7964FF5843B2%40dwheeler.com.
