Zulip Chat Archive

Stream: general

Topic: powers of a type


view this post on Zulip Johan Commelin (May 11 2018 at 14:00):

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?

view this post on Zulip Patrick Massot (May 11 2018 at 14:27):

Good question. I will need this as well.


Last updated: May 18 2021 at 16:25 UTC