lecopivo / scientific-computing-lean

work in progress book on Scientific Computing in Lean
https://lecopivo.github.io/scientific-computing-lean/
10 stars 2 forks source link

`#check (0 + 5 + 0) rewrite_by simp only [add_zero]` does not produce `0 + 5` #5

Open Seasawher opened 4 months ago

Seasawher commented 4 months ago

in Optimizing Array Expressions, it says that

#check (0 + 5 + 0) rewrite_by simp only [add_zero]

produces 0 + 5. but actually,

/-
5 : Nat
-/
#check (0 + 5 + 0) rewrite_by simp only [Nat.add_zero]