# Zulip Chat Archive

## Stream: general

### Topic: what is a numeral

#### Kevin Buzzard (Jan 15 2022 at 16:02):

My understanding is that `37`

is a numeral. Is `(37 : real)`

a numeral? My understanding is that `real.pi`

is not a numeral. Is `-37`

a numeral? Is `1/37`

a numeral? What is a numeral? I would not expect `norm_num`

to prove `pi>3`

but I would expect it to prove `1/37>0`

. The documentation of `norm_num`

says it proves theorems about `numerical expressions`

. Is the idea that `1/37`

is not a numeral but it's a "numerical expression"? Sorry for such weird questions, I'm writing notes for my course and I'd rather get things right the first time than have people complain that I'm not using terminology correctly.

#### Anne Baanen (Jan 15 2022 at 16:51):

By numeral, I mean a "numeric literal", so an expression denoting a fixed number that cannot be decomposed into subexpressions. So `37`

, `3.7`

, `0x25`

and `0b00100101`

are all numerals in Lean, `-37`

is not a numeral since it applies the `-`

operator to `37`

.

I believe @Rob Lewis introduced me to this term, so he may have a more authoritative opinion.

#### Anne Baanen (Jan 15 2022 at 16:53):

Presumably "numerical expressions" in this context means expressions consisting only of numerals and operators known to `norm_num`

.

#### Rob Lewis (Jan 15 2022 at 16:57):

"Cannot be decomposed into subexpressions" is maybe a bit off, since `37`

is built of applications of docs#bit0, docs#bit1, etc. In the Lean 3 context specifically, I'd say a numeral is either `has_zero.zero`

or a sequence of 0 or more applications of `bit0`

and `bit1`

to `has_one.one`

. The type class requirements on these defintions mean that this only make sense over a type with 0, 1, and +.

#### Anne Baanen (Jan 15 2022 at 16:58):

Then you wouldn't call `3.7`

a numeral?

#### Rob Lewis (Jan 15 2022 at 16:58):

`37`

, `0x25`

are numerals in this sense. `3.7`

is not, but it is a "numerical expression": a sequence of applications of ring operations to numerals.

#### Rob Lewis (Jan 15 2022 at 17:00):

So

Is the idea that 1/37 is not a numeral but it's a "numerical expression"?

is right.

#### Anne Baanen (Jan 15 2022 at 17:00):

Right, I should make clear that by "subexpressions" I mean subexpressions in the source code. In the way that `a + b`

can be decomposed into `a`

, `+`

and `b`

, but not into `has_add.add`

nor `nat.has_add`

.

#### Rob Lewis (Jan 15 2022 at 17:03):

At least in the original C++ implementation of `norm_num`

there was a third distinction, "generalized numerals" or something like that, which would have included `1/37`

and `-37`

. It's supposed to capture the notion of a fully reduced numeral expression.

#### Rob Lewis (Jan 15 2022 at 17:03):

Something like, "a numeral, or the negation of a numeral, or the division of two numerals, or the negation of the division of two numerals"

#### Rob Lewis (Jan 15 2022 at 17:04):

`norm_num`

applied to a numeral expression should produce a generalized numeral.

#### Kevin Buzzard (Jan 15 2022 at 17:34):

Thanks a lot for these comments!

#### Mario Carneiro (Jan 15 2022 at 18:48):

I believe I have used the term "rational numeral" or "integer numeral" to refer (in `norm_num`

docs) to what Rob calls "generalized numeral"

#### Mario Carneiro (Jan 15 2022 at 18:49):

so `1/3`

is a rational numeral but `2/6`

is not, and `-13`

is an integer numeral

#### Mario Carneiro (Jan 15 2022 at 18:50):

it is like "simp-normal form" but for `norm_num`

instead

#### Mario Carneiro (Jan 15 2022 at 18:50):

Usually, when I say numeral without qualification I mean natural numeral though, so `0`

or `1`

or `37`

but not `2+2`

or `-5`

#### Mario Carneiro (Jan 15 2022 at 18:53):

the term overlaps a lot with "numeric literal" which deals with the actual parser input, so for example `0x20`

is a hexadecimal literal and `32`

is a (decimal) numeric literal. I probably use the terms interchangeably most of the time

Last updated: Aug 03 2023 at 10:10 UTC