Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
import Game.MyNat.Multiplication
namespace MyNat
open MyNat
def pow : ℕ → ℕ → ℕ
| _, zero => one
| m, (succ n) => pow m n * m
instance : Pow ℕ ℕ where
pow := pow
-- notation a ^ b := pow a b
-- Important note: This here is the real `rfl`, not the weaker game version
example : (1 : ℕ) ^ 1 = 1 := by rfl
theorem pow_zero (m : ℕ) : m ^ 0 = 1 := by rfl
theorem pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := by rfl
def two_eq_succ_one : (2 : ℕ) = succ 1 := by rfl
end MyNat
