typo in Functional programming in Lean 8.4.5

Stream: general

[Asei Inoue]

I found a typo in FPiL 8.4.5

0 leqn → 0 \leq n

image.png

[Asei Inoue]

https://lean-lang.org/functional_programming_in_lean/Programming___-Proving___-and-Performance/More-Inequalities/#Functional-Programming-in-Lean--Programming___-Proving___-and-Performance--More-Inequalities

[Ruben Van de Velde]

https://github.com/leanprover/fp-lean/pull/213

[Asei Inoue]

PR is not welcome…？

[Asei Inoue]

@David Thrane Christiansen

[Ruben Van de Velde]

Well, that's... something.

[Kevin Buzzard]

Issues are welcome though!

[David Thrane Christiansen]

I'm considering changing that script.

The reason is that PRs that change content, rather than fixing things like typos, are really difficult to review - the book goes to great lengths to not use anything before introducing it, and this dependency order is subtle. And PRs that do some stylistic thing all over the place, where 70% of them are real improvements, are also extremely labor intensive to sort through.

[David Thrane Christiansen]

This doesn't really accord with peoples' expectations, though, so I think I'll get rid of it.

[David Thrane Christiansen]

Thanks

[Mauricio Collares]

A bot auto-rejection's probably easier to not take personally, though

[Mauricio Collares]

Doesn't GitHub allow you to hide the PR tab completely?

[David Thrane Christiansen]

Nope. All the others, yes, but not that one.

[David Thrane Christiansen]

I'll see how this goes without it