Define a decimal expansion constructor. The decimal expansions built with
this constructor are not meant to be used alone outside of this chapter.
Rather, they are meant to be used exclusively as part of a decimal number
with a decimal fraction, for example .
That decimal point operator is defined in the next section. The bulk of
these constructions have originally been proposed by David A. Wheeler on
12-May-2015, and discussed with Mario Carneiro in this thread:
https://groups.google.com/g/metamath/c/2AW7T3d2YiQ.