docgen problem

Stream: mathlib4

[Peter Nelson]

In the docs page for matroid contraction, references to Matroid.delete are spelt that way, even though the code uses notation for deletion.

For instance, Matroid.contract_dual : (M ／ X)✶ = M✶ ＼ X appears as Matroid.contract_dual : (M ／ X)✶ = M✶.delete X.

The notation for deletion is scoped notation, and is defined in Mathlib.Data.Matroid.Delete.

Can anyone tell me what is going on?

[Kyle Miller]

What's going on is that it's scoped notation. Currently scoped notations are not enabled when generating documentation, but it's planned.