has_pow nat

Stream: new members

[Benjamin FL]

Hi,
I'm trying to work through Theorem Proving in Lean, but running into an issue in Chapter 4. There's a snippet of code involving some #checks of powers of natural numbers which fails with the error "failed to synthesize type class instance for m n : ℕ ⊢ has_pow ℕ ℕ". Is there any way to fix this? I'm guessing I have to somehow teach Lean what it means to take powers of natural numbers in the same way that the snippet teaches Lean what it means for one natural to divide another?
Thanks for any help!
Ben Fayyazuddin Ljungberg

[Shing Tak Lam]

There used to be a definition of pow for natural numbers built into Lean, but there was quite a few issues with it, so it was removed from Lean. The definition of has_pow ℕ ℕ is now in mathlib, so if you add import data.nat.basic to the top of the file Lean should be able to find the instance.

[Johan Commelin]

Note that this change is like 3 days old. So the authors haven't caught up with it...

[Patrick Massot]

Oh, we're sorry about that. Nobody thought about checking that TPIL wasn't impacted byt this change. @Jeremy Avigad

[Benjamin FL]

Thanks for the quick responses, really appreciate it!

[Jeremy Avigad]

I'm on it -- I'll fix it soon.