mathlib3
refactor(data/list/min_max): use with_top for maximum and define argmax
#1320
Merged
Overview
Commits
7
Changes
View On GitHub

refactor(data/list/min_max): use with_top for maximum and define argmax #1320

mergify merged 7 commits into master from argmax
ChrisHughes24
ChrisHughes24 refactor(data/list/min_max): use option for maximum and define argmax
9a5a4f81
ChrisHughes24 ChrisHughes24 requested a review 6 years ago
ChrisHughes24 prove minimum_singleton
185f299e
ChrisHughes24 fix build
9bc81c69
urkud
urkud commented on 2019-08-13
ChrisHughes24 use with_bot for maximum
c8b977bd
ChrisHughes24 update comments
fe0bb35d
ChrisHughes24 ChrisHughes24 changed the title refactor(data/list/min_max): use option for maximum and define argmax refactor(data/list/min_max): use with_top for maximum and define argmax 6 years ago
cipher1024
cipher1024 approved these changes on 2019-08-19
cipher1024 cipher1024 added ready-to-merge
mergify[bot] Merge branch 'master' into argmax
8ae4f831
mergify[bot] Merge branch 'master' into argmax
a06783f9
mergify mergify merged 9eefd40e into master 6 years ago
mergify mergify deleted the argmax branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum