> On Nov 29, 2021, at 3:57 AM, Mario Carneiro <[email protected]> wrote:
>
> Late to the party, but I agree with Norm & Jim: Deductions can have 0
> hypotheses, and while there is a naming conflict between whether the xxxd
> theorem is the result of "deductionizing" (add "ph ->" to all hyps and
> conclusion) the corresponding xxx or xxxi theorem, this is a rare situation.
Also late to the party. An alternative would be to keep the definition of
"deduction form" & let the "d" suffix also be used in these other cases.
Before changing the definition of "deduction form" it'd be good to figure out
how to rewrite metamath book section 3.9.3 (deduction form)
and the corresponding HTML files on deduction. They all lean heavily into the
"one or more" definition.
I'm saying we can't change that, just that we'd need to rewrite those sections
to be consistent, and that may be trickier than
it first appears.
--- David A. Wheeler
--
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/C82E5928-EB00-4ED2-90EA-1B1F3C1E5A3A%40dwheeler.com.
