Oddity in online documentation for subsingletion

Stream: new members

[Jacques Carette]

At https://leanprover-community.github.io/mathlib_docs/core/init/logic.html#decidable.subsingleton if you expand out the Equations tab, there are 7 equations, which all are _ = _ (verbatim). Is this a bug?

[Bryan Gin-ge Chen]

Oh, that's funny. Maybe we need to tell Lean not to hide proof terms when generating the docs.

[Reid Barton]

what's the point of even generating these equations? I assume they're the equational lemmas, but if both sides are proofs...?

[Bryan Gin-ge Chen]

Yeah, filtering those out of the output of get_eqn_lemmas_for here might be a better idea.

[Reid Barton]

I think the equation compiler shouldn't even generate them (or generate them but then discard them)

[Jacques Carette]

Glad it wasn't just me then!