mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: add some docstrings to lemmas specialized to Nat and Int

Open fpvandoorn opened this issue 1 year ago • 4 comments

Open in Gitpod

fpvandoorn avatar Mar 26 '24 14:03 fpvandoorn

Thanks!

bprs d+

riccardobrasca avatar Mar 26 '24 14:03 riccardobrasca

bors d+

riccardobrasca avatar Mar 26 '24 14:03 riccardobrasca

:v: fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-bors[bot] avatar Mar 26 '24 14:03 mathlib-bors[bot]

bors merge

fpvandoorn avatar Mar 28 '24 11:03 fpvandoorn

It seems this was forgotten? I'll try again.

bors merge

fpvandoorn avatar Apr 04 '24 11:04 fpvandoorn

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar Apr 04 '24 13:04 mathlib-bors[bot]