mathlib3
docs(category_theory/limits): adding many docstrings
#2185

Merged

docs(category_theory/limits): adding many docstrings #2185

mergify merged 4 commits into master from limits_comments

lots of comments!

fc0e9ec9

remove #lint

ad4fdcf7

kim-em requested a review from

fpvandoorn 6 years ago

kim-em requested a review from

rwbarton 6 years ago

kim-em added awaiting-review

jcommelin commented on 2020-03-19

Apply suggestions from code review

e28652c1

jcommelin approved these changes on 2020-03-19

jcommelin removed awaiting-review

jcommelin added ready-to-merge

Merge branch 'master' into limits_comments

4a1f463d

mergify merged 1a398a72 into master 6 years ago

mergify deleted the limits_comments branch 6 years ago

Reviewers

jcommelin

fpvandoorn

rwbarton

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone