is_Type

Stream: metaprogramming / tactics

[Patrick Massot]

In Lean 3, how to test whether an element of the local context has type Type ??

[Yaël Dillies]

I think you can use infer_type your_variable to get an expr and then match for docs#expr.sort.

[Gabriel Ebner]

Or in short, expr.is_sort <$> infer_type hyp.

[Patrick Massot]

Silly me, I looked for expr.is_type but not expr.is_sort

[Patrick Massot]

Thanks!

[Patrick Massot]

Except that Lean pretends expr.is_sort doesn't exist

[Gabriel Ebner]

It's in mathlib. docs#expr.is_sort

[Patrick Massot]

I was missing an import