Rob Lewis
Rob Lewis
This isn't ready to be merged yet. I'm going to port `data.bool.basic` and improve those instances, which are necessary for the mathlib test case. Looking for comments on my implementation!
This was found by Joseph Rotella. The equation compiler fails to create a helper definition because of a universe error, even though the definition itself is sensible. ```lean -- fails...
This was found in class today by Joseph Rotella: ```lean def f : ∀ (α : Type), list α → unit | α [] := () | α ((y::ys)::xs) :=...
There were some amazing performance increases earlier this year from improved instance caching. I just noticed another situation where redundant searches are performed. Note that I don't really know the...
When I call `lean --make` I often don't care about the full output; either it succeeds, or there's an error, and I want to start fixing from the first error....
At https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Dots.20in.20outputs.20.2B.20documentation it was pointed out that we have no manual page listing all the configuration options. These options are at least slightly dynamic, in that users can create new...
In @hrmacbeth 's tutorial, there were examples of problems that `polyrith` could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a...
Thanks to work by @zhangir-azerbayev , we have a dataset of every declaration in (a recent version of) mathlib translated to natural language. People from OpenAI are interested in improving...
This will be linked to from https://github.com/leanprover-community/doc-gen/pull/168 cc @zhangir-azerbayev , any suggestions for the wording?