Bryan Gin-ge Chen
Bryan Gin-ge Chen
`decidable.to_bool` is `export`ed out of `decidable` [here](https://github.com/leanprover-community/lean/blob/4c40c41/library/init/logic.lean#L597), however, https://leanprover-community.github.io/mathlib_docs/find/to_bool doesn't work (cf. https://leanprover-community.github.io/mathlib_docs/find/decidable.to_bool). Noticed [in this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/equality.20function.20%28bool%29/near/210801004).
We're telling staticjinja that [every `.md` file is a jinja2 template](https://github.com/leanprover-community/leanprover-community.github.io/blob/1a7f9a90bfca81144ab4ffdfac9f7eebd9003487/make_site.py#L399-L421), so if one of them contains `{{` (e.g. when talking about "weakly implicit" arguments in Lean, (usually written `⦃`...
Cf. https://github.com/leanprover/lean4/issues/267
@EdAyers wrote some nice explanations of various aspects of Lean 3 in [his "edlib" repo](https://github.com/EdAyers/edlib/tree/master/docs), including e.g. an explanation of unicode in Lean and a series of articles on meta...
See [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/quotient.2Elift). (Though perhaps there's still more to discuss.)
[The section on variable conventions in our style doc](https://leanprover-community.github.io/contribute/style.html#variable-conventions) should be expanded to include e.g. fields, rings, categories, etc.
Requested by @digama0. https://github.com/leanprover-community/mathlib3 was archived on July 24, 2024, so we should have the mathlib3-related graphs on our [Mathlib statistics page](https://leanprover-community.github.io/mathlib_stats.html) end there too. Working on this will require...
### Description (Background info: I installed [oh my zsh](https://ohmyz.sh/) on a whim and one of the things it occasionally does is prompts the user if they'd like to update when...
In order to make effective use of the simplifier, among all the syntactically distinct propositionally equal / definitionally equal forms of some expression, we try to choose one that is...