powers of a type

Stream: general

[Johan Commelin]

I found myself typing \R^n into Lean, and it complained. I am still learning a lot about the type class system. Would it make sense to have an instance of has_pow Type \N, or would this create some unforseen problems?

[Patrick Massot]

Good question. I will need this as well.