Closed kbuzzard closed 4 years ago
Daniela 7 hours Small fix: the theorem list in Power World displays pow_succ (a b : mynat) : a ^ succ(b) = a ^ b b. I think that should be pow_succ (a b : mynat) : a ^ succ(b) = a ^ b a. It does behave correcly when used.
Fixed. Thanks.
kbuzzard
commented
4 years ago
Daniela 7 hours Small fix: the theorem list in Power World displays pow_succ (a b : mynat) : a ^ succ(b) = a ^ b b. I think that should be pow_succ (a b : mynat) : a ^ succ(b) = a ^ b a. It does behave correcly when used.