fix(library/init/core): closes #1951

- Add has_pow type class
- Make `^` notation right associative

library/data/bitvec.lean

@@ -190,7 +190,7 @@ section conversion
   : bitvec.to_nat (bitvec.of_nat k n) = n % 2^k :=
   begin
     induction k with k generalizing n,
-    { unfold pow, simp [nat.mod_one], refl },
+    { unfold pow nat.pow, simp [nat.mod_one], refl },
     { have h : 0 < 2, { apply le_succ },
       rw [ of_nat_succ
          , to_nat_append

library/init/core.lean

@@ -43,7 +43,7 @@ reserve infixl ` * `:70
 reserve infixl ` / `:70
 reserve infixl ` % `:70
 reserve prefix `-`:100
-reserve infix ` ^ `:80
+reserve infixr ` ^ `:80
 
 reserve infixr ` ∘ `:90                 -- input with \comp
 
@@ -337,7 +337,11 @@ class has_sep (α : out_param $ Type u) (γ : Type v) :=
 /- Type class for set-like membership -/
 class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α → γ → Prop)
 
+class has_pow (α : Type u) (β : out_param $ Type v) :=
+(pow : α → β → α)
+
 export has_andthen (andthen)
+export has_pow (pow)
 
 infix ∈        := has_mem.mem
 notation a ∉ s := ¬ has_mem.mem a s
@@ -360,6 +364,7 @@ infix ⊆        := has_subset.subset
 infix ⊂        := has_ssubset.ssubset
 infix \        := has_sdiff.sdiff
 infix ≈        := has_equiv.equiv
+infixr ^       := has_pow.pow
 
 export has_append (append)
 

library/init/data/nat/basic.lean

@@ -197,11 +197,12 @@ show succ (n + n) ≠ 0, from
 
 /- Exponentiation -/
 
-def pow (b : ℕ) : ℕ → ℕ
+protected def pow (b : ℕ) : ℕ → ℕ
 | 0        := 1
 | (succ n) := pow n * b
 
-infix `^` := pow
+instance : has_pow nat nat :=
+⟨nat.pow⟩
 
 lemma pow_succ (b n : ℕ) : b^(succ n) = b^n * b := rfl
 

tests/lean/run/1951.lean

@@ -0,0 +1,5 @@
+#eval 2 ^ (3 ^ 2)
+#eval 2 ^ 3 ^ 2
+
+example (a b c : nat) : a ^ (b ^ c) = a ^ b ^ c :=
+rfl

tests/lean/run/exhaustive_vm_impl_test.lean

@@ -103,7 +103,7 @@ run_cmd verify $ ∀ x < 100, ∀ y < 10, is_ok $ nat.test_bit x y
 
 def ints : list ℤ :=
 (do i ← list.range 40, [-i, i]) ++
-(do s ← [-1,1], j ← list.range 20, [s*2^31 + j-10])
+(do s ← [-1,1], j ← list.range 20, [s*(2^31:nat) + j-10])
 
 def small_ints : list ℤ :=
 (do i ← list.range 40, [-i, i])
@@ -124,4 +124,4 @@ run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.land x y
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.ldiff x y
 run_cmd verify $ ∀ x ∈ ints, is_ok $ int.lnot x
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.lxor x y
-run_cmd verify $ ∀ x ∈ ints, ∀ y < 10, is_ok $ int.test_bit x y
+run_cmd verify $ ∀ x ∈ ints, ∀ y < 10, is_ok $ int.test_bit x y

tests/lean/struct_class.lean.expected.out

@@ -16,6 +16,7 @@ has_mod : Type u → Type u
 has_mul : Type u → Type u
 has_neg : Type u → Type u
 has_one : Type u → Type u
+has_pow : Type u → out_param (Type v) → Type (max u v)
 has_sdiff : Type u → Type u
 has_sep : out_param (Type u) → Type v → Type (max u v)
 has_sizeof : Sort u → Sort (max 1 u)
@@ -43,6 +44,7 @@ has_mod : Type u → Type u
 has_mul : Type u → Type u
 has_neg : Type u → Type u
 has_one : Type u → Type u
+has_pow : Type u → out_param (Type v) → Type (max u v)
 has_sdiff : Type u → Type u
 has_sep : out_param (Type u) → Type v → Type (max u v)
 has_sizeof : Sort u → Sort (max 1 u)