typeof

Stream: Is there code for X?

[Eric Wieser]

Is there a builtin definition

def typeof {α : Type*} (x : α) := α

which would maybe be useful for casting as (a * b : typeof (x * y))?

[Simon Hudon]

I don't think that definition exists anywhere. Why do you want it to be builtin?

[Scott Morrison]

I'm having trouble imagining a use case where I don't already know that type.