Zulip Chat Archive
Stream: maths
Topic: chain rule
Patrick Massot (Mar 11 2022 at 16:08):
@Sebastien Gouezel is there any reason why x is an explicit argument in docs#has_fderiv_at.comp?
Sebastien Gouezel (Mar 12 2022 at 08:04):
Yes: at several places Lean was unable to infer it when it was implicit, so I switched from implicit to explicit to be able to help the system when needed.
Last updated: May 02 2025 at 03:31 UTC