Notation for numerals

Stream: new members

[Horatiu Cheval]

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]

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]

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

[Horatiu Cheval]

I see, thanks!

[Horatiu Cheval]

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]

def foo : has_add ℕ := ⟨λ x y, x + y + y + 37⟩

attribute [instance, priority 100000] foo

#reduce 2 -- 40
#reduce 40 -- 5773

[Kevin Buzzard]

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]

If you define has_div too you can support decimals too

[Eric Wieser]

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]

Just remember not to #check (0 : X)

[Horatiu Cheval]

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]

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]

Are you sure that's pure 5??

[Yakov Pechersky]

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

[Yakov Pechersky]

local notation `𝟢` := type.zero

#reduce (5 : type) -- (((𝟢↣𝟢)↣𝟢↣𝟢)↣(𝟢↣𝟢)↣𝟢↣𝟢)↣𝟢↣𝟢
#reduce _root_.pure 5 -- 𝟢↣𝟢↣𝟢↣𝟢↣𝟢↣𝟢

[Mario Carneiro]

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]

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