【Lean4】norm_num

norm_num

数値計算を自動化する

Plaintext

example : 2 + 3 = 5 := by
  norm_num

example : (7 : ℤ) ^ 2 = 49 := by
  norm_num

example : 2 + 3 = 5 := by
  norm_num

example : (7 : ℤ) ^ 2 = 49 := by
  norm_num

具体的な数の計算に向いている