According to our conventions (see section "Conventions" in set.mm):
"Deduction form" is the preferred form for theorems because this form
allows us to easily use the theorem in places where (in traditional
textbook formalizations) the standard Deduction Theorem (see below)
would be used. We call this approach <b>"deduction style"</b>.
In contrast, we usually avoid theorems in "inference form" when that
would end up requiring us to use the deduction theorem.
So adding ~fnconstd should be no problem, but adding ~fnconst ("inference
form", like ~fconst) should be avoided.
As said already before, such a theorem should be usually added to a mathbox
first.
--
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/d1d3b7cb-de96-4cc4-9ef5-4cc01a808fefn%40googlegroups.com.
