Commit 2026-03-21 09:03 576996fc

feat: add #check' command and tactic, which only show explicit arguments (#31194) In some areas (such as differential geometry), many lemmas have a lot of implicit and typeclass arguments. Using #check foo to determine which explicit arguments are expected for a given lemma gives output which is painful to read, because the explicit argument is buried among many lines of other output. The #check' command and tactic produce very similar output, but with implicit and typeclass arguments omitted. This increases usability a lot. In the future, this could (and should) be unified to the #check command in core, by becoming e.g. #check +only-explicit. Until then, let us add this to mathlib to facilitate experimentation of the most useful behaviour. From the project towards geodesics and the Levi-Civita connection.