Commit 2020-04-21 10:37 15d35b1a

feat(tactic/#simp): a user_command for #simp (#2446)

#simp 5 - 5

prints 0. If anyone knows how to get access to local variables while parsing an expression, that would be awesome. Then we could write

variable (x : ℝ)
#simp [exp_ne_zero] : deriv (λ x, (sin x) / (exp x)) x

as well as

#simp [exp_ne_zero] : λ x, deriv (λ x, (sin x) / (exp x)) x