Topic: powers of a type
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?
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