Common expressions for the theory of proveit.numbers.numerals

import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit.numbers.numerals.numeral import Numeral

%begin common

Defining common sub-expressions for theory 'proveit.numbers.numerals'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

zero, one, two, three, four, five, six, seven, eight, nine = [Numeral(n) for n in range(10)]

zero:

one:

two:

three:

four:

five:

six:

seven:

eight:

nine:

hexa, hexb, hexc, hexd, hexe, hexf = [Numeral(10+n, chr(ord('a') + n)) for n in range(6)]

hexa:

hexb:

hexc:

hexd:

hexe:

hexf:

%end common

These common expressions may now be imported from the theory package: proveit.numbers.numerals