Zulip Chat Archive

Stream: general

Topic: unused arguments linter and structures

Yury G. Kudryashov (Mar 04 2021 at 01:04):

It seems that the arguments [smooth_manifold_with_corners I M] and [smooth_manifold_with_corners I' M'] are unused in docs#times_cont_mdiff_map. Am I right that the "unused arguments" linter doesn't catch this because times_cont_mdiff_map is a structure?

Yury G. Kudryashov (Dec 23 2021 at 19:52):

@Johan Commelin Re: your comment on #10995

Yury G. Kudryashov (Dec 23 2021 at 19:53):

For times_cont_mdiff_maps, @Sebastien Gouezel says that nobody wants to deal with smooth maps between non-manifolds anyway.

Last updated: Dec 20 2023 at 11:08 UTC