binOpの自然数版

Lean 具体例

演算子優先度〈prec〉は適切かどうかわからない。

infix:70 "←" => Nat.pow

#eval 5 ← 2 -- 25

def sqPow (n:Nat) : Nat := n ← (n * n)
#eval sqPow 2 -- 16