## Stream: Is there code for X?

### Topic: typeof

#### Eric Wieser (Oct 03 2020 at 11:59):

Is there a builtin definition

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


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

#### Simon Hudon (Oct 03 2020 at 14:00):

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

#### Scott Morrison (Oct 04 2020 at 00:56):

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

Last updated: May 17 2021 at 16:26 UTC