Zulip Chat Archive

Stream: Is there code for X?

Topic: typeof


view this post on Zulip 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))?

view this post on Zulip Simon Hudon (Oct 03 2020 at 14:00):

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

view this post on Zulip 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