Stream: new members
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?
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.
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...?
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.
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)
Jacques Carette (Aug 25 2020 at 01:17):
Glad it wasn't just me then!
Last updated: May 09 2021 at 19:11 UTC