mathlib

mathlib copied to clipboard

The following snippet triggers the "missing doc string" complaint from the linter:

set_option old_structure_cmd true

/-- Foo structure -/
structure foo := (x : ℕ)

/-- Bar structure -/
structure bar extends foo := (y : ℕ)

#lint -- #print bar.to_foo /- def missing doc string -/

This is a minor issue and so far does not seem to have come up very often. @robertylewis gave a helpful summary of the situation here