Casts between identical types

Stream: new members

[Sébastien Boisgérault]

Hi everyone! :wave:

I was (naively?) expecting the notation (b : A) to convert a term of type B to type A when B is defined by

def B := A

In context:

def Pointer := Nat
def Size := Nat

def ptr : Pointer := (0 : Nat)
def size : Size := (512 : Nat)

#eval ptr + size -- fails as expected

#eval (ptr : Nat) + (size : Nat) -- too bad I was expecting this to work :(

def ptr_as_nat : Nat := ptr
#check ptr_as_nat -- Nat, as expected

def size_as_nat : Nat := size
#check size_as_nat -- Nat, as expected

#eval ptr_as_nat + size_as_nat -- OK

-- But
def ptr_as_nat' := (ptr : Nat)
#check ptr_as_nat' -- Pointer :(

Here the expression (ptr : Nat) is not rejected as incorrect, but doesn't perform the conversion I was expecting. What is it doing then? What should I do to perform the conversion? I'd like to avoid the explicit creation of intermediate variables like ptr_as_natif that's possible.

Cheers!

Sébastien

[Aaron Liu]

(b : A) instructs Lean to elaborate b as a term of type A, and then check to make sure that the result really has type A. To put a marker on b that says "I have type A", you can do show A from b instead.

[Sébastien Boisgérault]

Understood. Thank you! :pray: