Bolton Bailey
Bolton Bailey
When I run the command "Coq: Search" from the command palette, it opens a log called "Queries". But there is no output from search commands here. I'm seeing search command...
Per the discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20repeat/near/253898059), the `repeat { t }` tactic does not actually depend on whether or not `t` makes progress, and the iteration will terminate if `t` finishes a...
Add linear codes and defines the Reed-Solomon code. - [ ] depends on: #15689 --- [](https://gitpod.io/from-referrer/)
The links are broken, they should be relative to the semantics directory, not the top-level
> See [recipes/plain-lean4.lean](https://github.com/cpitclaudel/alectryon/blob/master/recipes/plain-lean4.lean), [recipes/lean4-tactics.rst](https://github.com/cpitclaudel/alectryon/blob/master/recipes/lean4-tactics.rst), [recipes/lean4-tactics-myst.md](https://github.com/cpitclaudel/alectryon/blob/master/recipes/lean4-tactics-myst.md) and [recipes/literate-lean4.lean](https://github.com/cpitclaudel/alectryon/blob/master/recipes/literate-lean4.lean) for examples. All of these links are giving me 404
**Describe the bug** A clear and concise description of what the bug is. When I create a constant from a nested array, the shape is not what I expect -...
~~A definition of mu-recursive functions (currently on the naturals).~~ It's my hope that this can be the start of computational complexity in mathlib. Anyone who is interested in seeing complexity...
A PR to prove that the parity of the number of roots of a real polynomial in a range depends on the signs of the evaluations of the polynomial on...
This small PR changes the error message that triggers when simp reaches the `maxSteps` parameter to mention that this is a configurable setting and say what the name of the...
Adds `modByMonic_eq_zero_iff_quotient_eq_zero` and `quotient_singleton_eq` --- [](https://gitpod.io/from-referrer/)