fix pretty-printing of Power. #46

leanprover-community · Dec 15, 2023 · a71cd97 · a71cd97
1 parent a126620
commit a71cd97
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Game/MyNat/Power.lean b/Game/MyNat/Power.lean
@@ -10,7 +10,7 @@ instance : Pow ℕ ℕ where
   pow := pow
 
 -- Note: since v4.2.0-rc2
-macro_rules | `($x ^ $y)   => `(Pow.pow $x ($y : MyNat))
+macro_rules | `($x ^ $y)   => `(HPow.hPow ($x : MyNat) ($y : MyNat))
 
 @[MyNat_decide]
 axiom pow_zero (m : ℕ) : m ^ 0 = 1