Zulip Chat Archive

Stream: new members

Topic: Oddity in online documentation for subsingletion


view this post on Zulip Jacques Carette (Aug 25 2020 at 00:29):

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?

view this post on Zulip Bryan Gin-ge Chen (Aug 25 2020 at 00:33):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 00:36):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 25 2020 at 00:39):

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

view this post on Zulip Reid Barton (Aug 25 2020 at 00:40):

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

view this post on Zulip Jacques Carette (Aug 25 2020 at 01:17):

Glad it wasn't just me then!


Last updated: May 09 2021 at 19:11 UTC