mathlib3
cleanup: replace `begin intros ...` with lambdas
#672

Merged

cleanup: replace `begin intros ...` with lambdas #672

cipher1024 merged 1 commit into master from remove-begin-intros

cleanup: replace `begin intros ...` with lambdas

ad37d382

cipher1024 requested a review from

digama0 7 years ago

cipher1024 assigned

cipher1024 7 years ago

cipher1024 removed review request from

digama0 7 years ago

cipher1024 requested a review from

cipher1024 7 years ago

digama0 approved these changes on 2019-02-02

cipher1024 approved these changes on 2019-02-02

cipher1024 merged fb601459 into master 7 years ago

kim-em deleted the remove-begin-intros branch 7 years ago

Reviewers

cipher1024

digama0

Assignees

cipher1024

Labels

None yet

Milestone

No milestone