What is \u?

Stream: new members

[Albert Jiang]

Absolute beginner question, but what is the \u operator on natural numbers? Thanks!

[Albert Jiang]

Somehow searching the documentation gives very little results maybe due to the operator search feature...

[Jireh Loreaux]

Do you mean ↑? This is coe. It is a coercion. In this case, it's the natural map ℕ → ℤ.

[Jireh Loreaux]

Note, coercions can exist between lots of different types, so ↑ is not always this map (it depends on the source and target types).

[Albert Jiang]

Ah I see! Thank you! So it just converts the type of the operand in the most intuitive way?

[Jireh Loreaux]

sorry, I implicitly assumed the output type was ℤ, but you didn't say that, so what you are looking at may even be a different coercion.

[Albert Jiang]

Oh so it does convert the type depending on the type expected. Awesome!

[Albert Jiang]

Thanks!

[Jireh Loreaux]

It can't convert any type to any other type, it only works for for types with a coercion defined.

[Albert Jiang]

I'm looking at a case from nat to int :)

[Jireh Loreaux]

You need a has_coe_t (or has_coe) instance between the types. docs#has_coe_t

[Jireh Loreaux]

If you look at the docs for that and then click the "instances" arrow, you'll see the list of coercions. For example, you'll see nat.cast_coe which actually gives a coercion from ℕ to any type α with a zero, a one, and addition.

[Kyle Miller]

One neat thing is that Lean will insert coercions for you when types don't match up:

def foo (x : ℕ) : ℤ := x

#print foo
/-
def foo : ℕ → ℤ :=
λ (x : ℕ), ↑x
-/

This occurs while the elaborator is trying to take your expression and fill out all the missing details before it hands it off to the kernel for a final check.

[Kyle Miller]

You can turn this feature off:

set_option elaborator.coercions false

def foo (x : ℕ) : ℤ := x
/-
type mismatch, term
  x
has type
  ℕ
but is expected to have type
  ℤ
-/

[Kyle Miller]

Here's a way you can experimentally check what the coercion is from within Lean:

example (n : ℕ) : false :=
begin
  set m : ℤ := n with h,
  unfold_coes at h,
  /-
  n : ℕ,
  m : ℤ := ↑n,
  h : m = int.of_nat n
  ⊢ false
  -/
end

[Kyle Miller]

I guess the constructor docs#int.of_nat takes priority over docs#nat.cast_coe. The coercion is defined right here: https://github.com/leanprover-community/lean/blob/master/library/init/data/int/basic.lean#L21

[Jireh Loreaux]

Also, if you are using VS Code, in the widget panel you can click on the ↑ in the tactic state to see which coercion is being used.