Does `↑` ever do anything

Stream: new members

[Markus Schmaus]

I learnt about ↑ in Functional Programming in Lean: Coercion, it says:

Additionally, coercions can be manually inserted using an up arrow:

def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) :=
  ↑(392 : Nat)

In some cases, this can be used to ensure that Lean finds the right instances. It can also make the programmer's intentions more clear.

I never knew what this means concretely and I don't think I have come across any case in which writing ↑ makes a difference, particularly here are two cases in which I thought it would make a difference, but it doesn't:

def oneS : Subtype fun x : Nat => x = 1 := ⟨1, rfl⟩
def twoS : Subtype fun x : Nat => x = 2 := ⟨2, rfl⟩
#check ↑oneS + ↑twoS -- fails, doesn't coerce to Nat

def one : Nat := 1
def two : Nat := 2
#check ↑one + ↑two -- wroks, no coercion is apparent

Does anybody know a case in which writing ↑ changes the meaning of the code? Or is this just meant for the delaborator, which can use this symbol to inform the user that a conversion occurs at this location?

[Ruben Van de Velde]

Perhaps (↑(a + b) : \R) vs ((a + b) : \R)