doc-string puzzle

Stream: mathlib4

[Damiano Testa]

How would you conclude the doc-string for docs#CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork ?

Auxiliary definition for ran_isSheaf_of_isCocontinuous: if G : C ⥤ D is a cocontinuous functor...

[Kim Morrison]

Pinging file authors @Andrew Yang and @Joël Riou.

[Bryan Gin-ge Chen]

Related PR: #22058 (which looks like it's already about to be merged)

[Damiano Testa]

Ah, yes, sorry I was going to post the PR number, but I got distracted by a bug that Eric found in a different PR!

[Joël Riou]

Damiano Testa said:

How would you conclude the doc-string for docs#CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork ?

Auxiliary definition for ran_isSheaf_of_isCocontinuous: if G : C ⥤ D is a cocontinuous functor...

I would only keep "Auxiliary definition for ran_isSheaf_of_isCocontinuous".

[Damiano Testa]

Thanks! I'll update the doc-string once #22058 get merged.

[Damiano Testa]

#22067

[Damiano Testa]

Here are a couple more issues with doc-strings:

• docs#Lean.Meta.RefinedDiscrTree.DTExpr.isSpecific is missing a doc-string (pinging @Jovan Gerbscheid as the author of the file);
• Mathlib/Tactic/FunProp/Theorems.lean contains several declarations that have /-- -/ as doc-string (pinging @Tomas Skrivan as the author of the file):
  • docs#Mathlib.Meta.FunProp.FunctionTheorems
  • docs#Mathlib.Meta.FunProp.FunctionTheoremsExt
  • docs#Mathlib.Meta.FunProp.getTheoremsForFunction
• docs#Mathlib.Meta.FunProp.FunPropDeclsExt

If anyone can volunteer doc-strings for the missing declarations, please either PR them or let me know and I will!