# Zulip Chat Archive

## Stream: new members

### Topic: Notation for numerals

#### Horatiu Cheval (Mar 12 2021 at 19:53):

Is there a notational typeclass that enables me to use numeral notation `0, 1, 2, ...`

for a custom type? I only know about `has_zero`

but that only deals with the symbol `0`

.

#### Kevin Buzzard (Mar 12 2021 at 19:53):

You also need `has_one`

and `has_add`

, and Lean will take it from there.

```
constant X : Type
#check (37 : X)
/-
failed to synthesize type class instance for
⊢ has_one X
scratch2.lean:3:8
failed to synthesize type class instance for
⊢ has_add X
All Messages (3)
-/
```

#### Yakov Pechersky (Mar 12 2021 at 19:55):

And numerals to make true sense, I really hope addition in your type is associative.

#### Horatiu Cheval (Mar 12 2021 at 19:57):

I see, thanks!

#### Horatiu Cheval (Mar 12 2021 at 20:01):

I actually didn't intend to have an addition for this, I only want some particular terms denoted by `0, 1, 2, ...`

, (I only have a meaningful successor notion, for some subset of terms), so not every term is equal to a numeral in this sense.

#### Kevin Buzzard (Mar 12 2021 at 20:01):

```
def foo : has_add ℕ := ⟨λ x y, x + y + y + 37⟩
attribute [instance, priority 100000] foo
#reduce 2 -- 40
#reduce 40 -- 5773
```

#### Kevin Buzzard (Mar 12 2021 at 20:02):

well each term is encoded in binary, so you need to make sure that 2 = 1 + 1 for your definition of 1 and add, etc. You might be better off defining `zero`

, `one`

, `two`

:-) Most types (like the reals) have the property that numerals work but not every terms is equal to a numeral.

#### Eric Wieser (Mar 12 2021 at 20:04):

If you define `has_div`

too you can support decimals too

#### Eric Wieser (Mar 12 2021 at 20:05):

Hey, lean has binary!

```
variables (X : Type) [has_add X] [has_div X] [has_one X]
#check (0b10100 : X)
#check (0xFF : X)
#check (2.5 : X)
```

#### Kevin Buzzard (Mar 12 2021 at 20:09):

Just remember not to `#check (0 : X)`

#### Horatiu Cheval (Mar 12 2021 at 20:22):

Ok, thank you all for the insights! Now after playing a little I realized the initial question wasn't really the best suited for my case. So, I have this:

```
inductive type
| zero : type
| arrow : type → type → type
infixr `↣` : 50 := type.arrow
def pure : ℕ → type
| 0 := type.zero
| (n + 1) := type.zero ↣ pure n
```

Can I, for an `n : ℕ`

, simply write `n`

to mean `pure n`

in a place where a `type`

is expected? (I realize it's kind of pointless here, but still, out of curiosity)

#### Yakov Pechersky (Mar 12 2021 at 20:25):

```
inductive type
| zero : type
| arrow : type → type → type
infixr `↣` : 50 := type.arrow
def pure : ℕ → type
| 0 := type.zero
| (n + 1) := type.zero ↣ pure n
instance : has_zero type := ⟨pure 0⟩
instance : has_one type := ⟨pure 1⟩
instance : has_add type := ⟨type.arrow⟩
example : type := 5
```

#### Kevin Buzzard (Mar 12 2021 at 20:26):

Are you sure that's `pure 5`

??

#### Yakov Pechersky (Mar 12 2021 at 20:27):

Ah, you're right, it's not.

#### Yakov Pechersky (Mar 12 2021 at 20:27):

```
local notation `𝟢` := type.zero
#reduce (5 : type) -- (((𝟢↣𝟢)↣𝟢↣𝟢)↣(𝟢↣𝟢)↣𝟢↣𝟢)↣𝟢↣𝟢
#reduce _root_.pure 5 -- 𝟢↣𝟢↣𝟢↣𝟢↣𝟢↣𝟢
```

#### Mario Carneiro (Mar 12 2021 at 20:37):

```
def type.append : type → type → type
| type.zero t := t
| (t1 ↣ t2) t := t1 ↣ t2.append t
instance : has_add type := ⟨type.append⟩
example : 5 = _root_.pure 5 := rfl
```

#### Kevin Buzzard (Mar 12 2021 at 20:59):

Oh nice, I couldn't figure it out :-)

Last updated: May 13 2021 at 05:21 UTC