CI Help

Stream: mathlib4

[Dominic Steinitz]

CI is complaining about this

https://github.com/leanprover-community/mathlib4/pull/34129/files#diff-ba91f3e90abd9f58020a6a18aeb59c2c4d273529f4b801eca1cfc0f7718be71aR63

/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Geometry/Manifold/EhresmannConnection.lean:63:3: error: @EhresmannConnection.horizontal definition missing documentation string

But I have a documentation string

https://github.com/leanprover-community/mathlib4/blob/e38629881df7da348291e497e9f5d28d0c430c33/Mathlib/Geometry/Manifold/EhresmannConnection.lean#L51

So I am now scratching my head :face_with_monocle:

[Michael Rothgang]

You need to document the definition itself, as well as all data fields of the structure. (For proof-valued fields, these are optional - but can be useful also.)