mathlib3
chore(*): pass dup_namespace and def_lemma lint tests
#1599

Merged

chore(*): pass dup_namespace and def_lemma lint tests #1599

mergify merged 10 commits into master from lint_mathlib

chore(*): pass dup_namespace and def_lemma lint tests

53172dfd

robertylewis commented on 2019-10-23

jcommelin commented on 2019-10-23

rwbarton commented on 2019-10-23

Update src/group_theory/free_group.lean

527a1e16

Update src/number_theory/pell.lean

4986f0eb

Update src/order/lattice.lean

6cf339d9

jcommelin commented on 2019-10-23

Update src/set_theory/ordinal.lean

a1d43e60

Update src/set_theory/ordinal.lean

ee000c0e

Update src/tactic/transfer.lean

339bc705

rwbarton commented on 2019-10-23

Update src/group_theory/free_group.lean

31b45a81

using nolint

fed35be7

kim-em approved these changes on 2019-10-24

kim-em added ready-to-merge

Merge branch 'master' into lint_mathlib

1877bf74

mergify merged 4b9cdf44 into master 6 years ago

mergify deleted the lint_mathlib branch 6 years ago

Reviewers

kim-em

rwbarton

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone