ITADN

the outputs of `∂ ... rewrite_by fun_trans` and `∂!` are different

#52OpenSeasawher 创建于 2024-12-22
S
Seasawhercommented
Thank you for creating a nice library! [Scientific Computing in Lean](https://lecopivo.github.io/scientific-computing-lean/-Differentiation/Symbolic-Differentiation/#Scientific-Computing-in-Lean---Differentiation--Symbolic-Differentiation--Notation) says that > Writing rewrite_by fun_trans every time we want to diferentiate an expression gets a bit tedious. We can add an exclamation mark after ∂ to indicate that we want to run fun_trans tactic to compute the derivative. However, in the following example `∂ ... rewrite_by fun_trans` and `∂! ` have different outputs. ```lean import SciLean.Analysis.Calculus.Notation.Deriv import SciLean.Analysis.Scalar.Notation open SciLean Scalar set_default_scalar ℝ variable {x y : ℝ} #check let g : ℝ → ℝ → ℝ := fun x y => x^2 + y^2 ∂ x, ((∂ x, (g x y)) x) rewrite_by fun_trans #check let g : ℝ → ℝ → ℝ := fun x y => x^2 + y^2 ∂! x, ((∂! x, (g x y)) x) ``` This is because `∂! `'s bug?
1 条评论