typeof

Stream: new members

[Steven Shaw]

Hi. I'm wondering if there might be a typeOf operator in Lean. I might want to confirm the type of an expression using an example, something like:

example: typeOf (String.append) = (String → String → String) := rfl

[Scott Morrison]

def typeOf {α} (_ : α) := α

example : typeOf String.append = (String → String → String) := rfl

[Kyle Miller]

There should be a typeof% "function" that gives you the type itself. I don't remember if it has an underscore in the name (on my phone)

[Steven Shaw]

Thanks, it's great to see how typeOf can be implemented in Lean itself. As for the built-in function, it looks like it's type_of%. I can't navigate to its definition, so I imagine it's a compiler intrinsic.

[Kyle Miller]

It's called a "term elaborator" and it's something you can even write yourself! (It's like a compiler intrinsic that's a macro)

[Mario Carneiro]

Go to definition should work on it, but you need to have import Lean so that the declaration is in the environment

[Steven Shaw]

Thanks, using import Lean, I can now navigate to the definition!