pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ git clean -dffx
pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ lake exe cache get
^C
pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '3c125512032771407147a2b35348eb1f4c3a12ba'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '1622a8693b31523c8f82db48e01b14c74bc1f155'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '9cb79405471ae931ac718231d6299bfaffef9087'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '07f60e90998dfd6592688a14cd67bd4e384b77b2'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '79402ad9ab4be9a2286701a9880697e2351e4955'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '8ce422eb59adf557fac184f8b1678c75fa03075c'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
No files to download
Decompressing 5824 file(s)
Unpacked in 111088 ms
Completed successfully!
pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ ls -al
total 40
drwxrwxr-x  5 pthomas pthomas 4096 Jan  5 10:30 .
drwxrwxr-x 12 pthomas pthomas 4096 Jan  4 23:33 ..
drwxrwxr-x  2 pthomas pthomas 4096 Jan  5 09:12 BatteriesExtraLean
-rw-rw-r--  1 pthomas pthomas  174 Jan  4 23:15 BatteriesExtraLean.lean
drwxrwxr-x  8 pthomas pthomas 4096 Jan  5 10:28 .git
-rw-rw-r--  1 pthomas pthomas    7 Jan  4 23:15 .gitignore
drwxrwxr-x  3 pthomas pthomas 4096 Jan  5 10:30 .lake
-rw-rw-r--  1 pthomas pthomas  510 Jan  4 23:39 lakefile.lean
-rw-rw-r--  1 pthomas pthomas 3134 Jan  4 23:16 lake-manifest.json
-rw-rw-r--  1 pthomas pthomas   29 Jan  4 23:16 lean-toolchain
pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ git status
On branch main
Your branch is up to date with 'origin/main'.

nothing to commit, working tree clean
pthomas@HP-Laptop:~/Desktop/github/lean/batteries_extra_lean$ lake build
⚠ [291/493] Built Mathlib.Control.Combinators
warning: ././.lake/packages/mathlib/././Mathlib/Control/Combinators.lean:35:4: `Monad.mapM'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Control/Combinators.lean:57:4: `Monad.sequence'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [345/493] Built Mathlib.Data.Prod.PProd
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/PProd.lean:35:8: `PProd.forall'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/PProd.lean:38:8: `PProd.exists'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [364/493] Built Mathlib.Tactic.Lift
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/Lift.lean:49:9: `PiSubtype.canLift'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [365/493] Built Mathlib.Logic.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:150:8: `dec_em'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:154:8: `em'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:299:8: `or_congr_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:302:8: `or_congr_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:315:8: `imp_or'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:354:8: `xor_iff_not_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:417:8: `eqRec_heq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:514:8: `forall_true_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:535:8: `exists_apply_eq_apply'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:542:6: `exists_apply_eq_apply2'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:551:6: `exists_apply_eq_apply3'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:578:8: `forall_apply_eq_imp_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:581:8: `forall_eq_apply_imp_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:641:8: `forall_prop_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:714:6: `Classical.choose_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:851:8: `dite_eq_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Basic.lean:855:8: `ite_eq_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [367/493] Built Mathlib.Data.List.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Defs.lean:241:9: `List.decidableChain'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [378/493] Built Mathlib.Logic.Function.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:85:8: `Function.Injective.eq_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:94:8: `Function.Injective.ne_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:124:8: `Function.Injective.of_comp_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:170:8: `Function.Surjective.of_comp_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:244:8: `Function.Bijective.of_comp_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:552:8: `Function.update_comp_eq_of_forall_ne'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:563:8: `Function.update_comp_eq_of_injective'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:660:8: `Function.extend_apply'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Basic.lean:692:8: `Function.Injective.surjective_comp_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [379/493] Built Mathlib.Data.Bool.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Bool/Basic.lean:157:8: `Bool.eq_true_of_not_eq_false'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Bool/Basic.lean:160:8: `Bool.eq_false_of_not_eq_true'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [381/493] Built Mathlib.Data.Sigma.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Sigma/Basic.lean:90:6: `Sigma.exists'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Sigma/Basic.lean:93:6: `Sigma.forall'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [382/493] Built Mathlib.Logic.IsEmpty
warning: ././.lake/packages/mathlib/././Mathlib/Logic/IsEmpty.lean:37:9: `Fin.isEmpty'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [385/493] Built Mathlib.Data.FunLike.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/FunLike/Basic.lean:188:8: `DFunLike.ext'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [391/493] Built Mathlib.Logic.Function.Iterate
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Iterate.lean:160:8: `Function.iterate_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Function/Iterate.lean:163:8: `Function.iterate_succ_apply'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [394/493] Built Mathlib.Logic.Unique
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Unique.lean:136:18: `Unique.subsingleton_unique'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Unique.lean:264:9: `Unique.subtypeEq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [395/493] Built Mathlib.Logic.Relation
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Relation.lean:351:8: `Relation.TransGen.head'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Relation.lean:354:8: `Relation.TransGen.tail'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Relation.lean:444:8: `Relation.TransGen.lift'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Relation.lean:453:6: `Relation.TransGen.closed'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Relation.lean:523:8: `Relation.ReflTransGen.lift'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [400/493] Built Mathlib.Data.Option.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:80:8: `Option.none_bind'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:84:8: `Option.some_bind'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:87:8: `Option.bind_eq_some'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:96:8: `Option.bind_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:103:8: `Option.bind_eq_bind'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:110:8: `Option.map_coe'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:140:8: `Option.map_bind'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:207:8: `Option.some_orElse'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:211:8: `Option.none_orElse'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:214:8: `Option.orElse_none'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:229:8: `Option.guard_eq_some'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:276:8: `Option.orElse_eq_some'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Option/Basic.lean:287:8: `Option.orElse_eq_none'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [405/493] Built Mathlib.Data.Prod.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/Basic.lean:34:8: `Prod.forall'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/Basic.lean:37:8: `Prod.exists'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/Basic.lean:54:8: `Prod.map_apply'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/Basic.lean:57:8: `Prod.map_fst'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Prod/Basic.lean:60:8: `Prod.map_snd'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [408/493] Built Mathlib.Data.Quot
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:595:18: `Quotient.liftOn'_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:599:14: `Quotient.surjective_liftOn'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:610:18: `Quotient.liftOn₂'_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:676:8: `Quotient.hrecOn'_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:689:8: `Quotient.hrecOn₂'_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:702:8: `Quotient.map'_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:709:8: `Quotient.exact'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:713:8: `Quotient.sound'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:717:18: `Quotient.eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:721:18: `Quotient.eq''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:726:8: `Quotient.out_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Quot.lean:729:8: `Quotient.mk_out'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [410/493] Built Mathlib.Logic.Equiv.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:140:9: `Equiv.inhabited'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:155:8: `Equiv.left_inv'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:156:8: `Equiv.right_inv'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:729:16: `Equiv.forall_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:741:16: `Equiv.exists_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:761:16: `Equiv.existsUnique_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:776:18: `Equiv.forall₂_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Defs.lean:786:18: `Equiv.forall₃_congr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [411/493] Built Mathlib.Algebra.Group.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Defs.lean:576:33: `pow_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Defs.lean:581:6: `pow_mul_comm'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Defs.lean:590:6: `pow_three'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Defs.lean:613:6: `pow_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [415/493] Built Mathlib.Data.Nat.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:97:6: `Nat.succ_pos'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:273:16: `Nat.sub_eq_of_eq_add'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:275:16: `Nat.eq_sub_of_add_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:278:16: `Nat.lt_sub_iff_add_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:280:16: `Nat.sub_lt_iff_lt_add'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:363:6: `Nat.mul_lt_mul''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:409:6: `Nat.le_div_iff_mul_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:412:6: `Nat.div_lt_iff_lt_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:456:16: `Nat.mul_div_cancel_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:508:16: `Nat.div_le_of_le_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:522:16: `Nat.div_le_self'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:624:6: `Nat.one_le_pow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:630:6: `Nat.one_lt_pow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:638:6: `Nat.one_lt_two_pow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:731:6: `Nat.leRec_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:775:6: `Nat.leRecOn_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:882:6: `Nat.decreasingInduction_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:1064:6: `Nat.mod_add_div'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:1066:6: `Nat.div_add_mod'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:1156:6: `Nat.mul_add_mod'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Nat/Defs.lean:1172:6: `Nat.dvd_sub'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [420/493] Built Mathlib.Order.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:71:8: `le_trans'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:74:8: `lt_trans'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:77:8: `lt_of_le_of_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:80:8: `lt_of_lt_of_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:92:8: `lt_of_le_of_ne'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:97:8: `Ne.lt_of_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:155:8: `le_of_le_of_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:158:8: `le_of_eq_of_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:161:8: `lt_of_lt_of_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:164:8: `lt_of_eq_of_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:264:8: `LT.lt.ne'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:350:8: `min_def'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:359:8: `max_def'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:402:8: `lt_iff_lt_of_le_iff_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:420:8: `le_of_forall_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:429:8: `le_of_forall_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:432:8: `forall_lt_iff_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:881:8: `update_le_update_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:940:8: `min_rec'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Basic.lean:943:8: `max_rec'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [422/493] Built Mathlib.Data.Int.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Data/Int/Defs.lean:191:16: `Int.add_le_zero_iff_le_neg'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Int/Defs.lean:193:16: `Int.add_nonnneg_iff_neg_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Int/Defs.lean:324:14: `Int.natAbs_ofNat'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Int/Defs.lean:572:6: `Int.toNat_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [427/493] Built Mathlib.Order.Compare
warning: ././.lake/packages/mathlib/././Mathlib/Order/Compare.lean:219:8: `Eq.cmp_eq_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [428/493] Built Mathlib.Data.List.Pairwise
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Pairwise.lean:54:8: `List.pairwise_map'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [430/493] Built Mathlib.Order.RelClasses
warning: ././.lake/packages/mathlib/././Mathlib/Order/RelClasses.lean:32:8: `antisymm'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/RelClasses.lean:109:8: `ne_of_irrefl'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [431/493] Built Mathlib.Algebra.Group.Hom.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Hom/Defs.lean:410:8: `map_div'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Hom/Defs.lean:415:6: `map_comp_div'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Hom/Defs.lean:463:8: `map_zpow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Hom/Defs.lean:469:6: `map_comp_zpow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Hom/Defs.lean:845:18: `MonoidHom.map_zpow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [432/493] Built Mathlib.Order.BoundedOrder.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Order/BoundedOrder/Basic.lean:142:8: `Ne.lt_top'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/BoundedOrder/Basic.lean:305:8: `Ne.bot_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [434/493] Built Mathlib.Order.Monotone.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Order/Monotone/Basic.lean:477:8: `Subsingleton.monotone'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Monotone/Basic.lean:480:8: `Subsingleton.antitone'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Monotone/Basic.lean:569:18: `StrictMono.ite'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Monotone/Basic.lean:587:18: `StrictAnti.ite'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [436/493] Built Mathlib.Algebra.Group.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:165:8: `mul_rotate'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:331:8: `mul_div_assoc'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:448:6: `inv_zpow'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:493:6: `zpow_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:519:8: `inv_div'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:530:8: `inv_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:710:8: `div_self'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:724:8: `eq_div_of_mul_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:727:8: `div_eq_of_eq_mul''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:770:8: `eq_div_iff_mul_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:872:8: `zpow_eq_zpow_emod'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:918:8: `div_eq_of_eq_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:927:8: `eq_div_of_mul_eq''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:930:8: `eq_mul_of_div_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:933:8: `mul_eq_of_eq_div'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:937:8: `div_div_self'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:950:8: `eq_div_iff_mul_eq''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:953:8: `div_eq_iff_eq_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Group/Basic.lean:981:8: `div_mul_div_cancel'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [439/493] Built Mathlib.Data.List.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:227:8: `List.replicate_right_inj'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:254:8: `List.reverse_cons'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:257:8: `List.reverse_concat'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:294:8: `List.getLast_append'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:300:8: `List.getLast_concat'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:304:8: `List.getLast_singleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:612:6: `List.cons_sublist_cons'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:760:8: `List.ext_get?'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:779:8: `List.ext_get?_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:827:8: `List.get_reverse'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1059:8: `List.takeI_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1083:8: `List.takeD_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1114:8: `List.foldl_fixed'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1118:8: `List.foldr_fixed'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1298:8: `List.foldl_eq_of_comm'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1302:8: `List.foldl_eq_foldr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1312:8: `List.foldr_eq_of_comm'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1625:8: `List.lookmap_id'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1702:8: `List.filter_subset'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1736:6: `List.map_filter'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:1741:6: `List.filter_attach'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:2080:8: `List.map₂Left_eq_map₂Left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:2119:8: `List.map₂Right_eq_map₂Right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:2153:8: `List.zipLeft_eq_zipLeft'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Basic.lean:2189:8: `List.zipRight_eq_zipRight'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [443/493] Built Mathlib.Data.List.Lattice
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Lattice.lean:111:8: `List.inter_nil'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [445/493] Built Mathlib.Logic.Equiv.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Logic/Equiv/Basic.lean:1707:8: `Equiv.coe_piCongr'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [446/493] Built Mathlib.Data.List.Forall2
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Forall2.lean:108:8: `List.left_unique_forall₂'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Forall2.lean:116:8: `List.right_unique_forall₂'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [447/493] Built Mathlib.Order.Disjoint
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:143:8: `Disjoint.inf_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:149:8: `Disjoint.inf_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:157:8: `Disjoint.of_disjoint_inf_of_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:273:6: `Codisjoint.ne_bot_of_ne_top'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:308:8: `Codisjoint.sup_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:314:8: `Codisjoint.sup_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Disjoint.lean:323:8: `Codisjoint.of_codisjoint_sup_of_le'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [451/493] Built Mathlib.Order.WithBot
warning: ././.lake/packages/mathlib/././Mathlib/Order/WithBot.lean:380:8: `WithBot.le_coe_unbot'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [452/493] Built Mathlib.Algebra.Order.Monoid.Unbundled.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:63:8: `mul_le_mul_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:68:8: `le_of_mul_le_mul_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:76:8: `mul_le_mul_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:82:8: `le_of_mul_le_mul_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:118:8: `mul_lt_mul_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:123:8: `lt_of_mul_lt_mul_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:129:8: `mul_lt_mul_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:135:8: `lt_of_mul_lt_mul_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:192:8: `mul_le_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:259:8: `mul_left_cancel''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:264:8: `mul_right_cancel''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:334:8: `max_mul_mul_le_max_mul_max'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:339:8: `min_mul_min_le_min_mul_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:356:8: `le_mul_of_one_le_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:363:8: `mul_le_of_le_one_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:370:8: `le_mul_of_one_le_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:377:8: `mul_le_of_le_one_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:406:8: `le_mul_iff_one_le_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:412:8: `le_mul_iff_one_le_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:418:8: `mul_le_iff_le_one_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:424:8: `mul_le_iff_le_one_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:436:8: `lt_mul_of_one_lt_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:443:8: `mul_lt_of_lt_one_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:450:8: `lt_mul_of_one_lt_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:458:8: `mul_lt_of_lt_one_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:488:8: `lt_mul_iff_one_lt_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:494:8: `lt_mul_iff_one_lt_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:499:8: `mul_lt_iff_lt_one_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:505:8: `mul_lt_iff_lt_one_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:556:8: `mul_lt_of_lt_of_lt_one'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:646:8: `lt_mul_of_lt_of_one_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:736:8: `mul_lt_of_lt_one_of_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:829:8: `lt_mul_of_one_lt_of_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1082:8: `Monotone.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1086:8: `MonotoneOn.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1090:8: `Antitone.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1094:8: `AntitoneOn.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1098:8: `Monotone.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1102:8: `MonotoneOn.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1106:8: `Antitone.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1110:8: `AntitoneOn.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1144:8: `StrictMono.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1148:8: `StrictMonoOn.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1153:8: `StrictAnti.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1157:8: `StrictAntiOn.const_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1168:8: `StrictMono.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1172:8: `StrictMonoOn.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1177:8: `StrictAnti.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1181:8: `StrictAntiOn.mul_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1281:8: `cmp_mul_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean:1287:8: `cmp_mul_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [453/493] Built Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean:51:21: `exists_one_lt_mul_of_lt'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean:77:8: `le_of_forall_one_lt_lt_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean:81:8: `le_iff_forall_one_lt_lt_mul'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [455/493] Built Mathlib.Algebra.Order.Sub.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/Sub/Defs.lean:200:8: `le_add_tsub'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [457/493] Built Mathlib.Order.Heyting.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Order/Heyting/Basic.lean:380:8: `sdiff_le_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Heyting/Basic.lean:431:8: `sup_sdiff_cancel'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Heyting/Basic.lean:766:8: `top_sdiff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [458/493] Built Mathlib.Order.Hom.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Order/Hom/Basic.lean:1082:8: `OrderIso.map_bot'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Hom/Basic.lean:1091:8: `OrderIso.map_top'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [459/493] Built Mathlib.Order.BooleanAlgebra
warning: ././.lake/packages/mathlib/././Mathlib/Order/BooleanAlgebra.lean:287:8: `sdiff_eq_self_iff_disjoint'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/BooleanAlgebra.lean:337:8: `sdiff_sdiff_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/BooleanAlgebra.lean:367:8: `sdiff_sdiff_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/BooleanAlgebra.lean:379:8: `sdiff_sdiff_sup_sdiff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/BooleanAlgebra.lean:524:8: `inf_compl_eq_bot'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [460/493] Built Mathlib.Order.SymmDiff
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:80:8: `symmDiff_eq_Xor'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:286:8: `symmDiff_top'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:289:8: `top_symmDiff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:349:8: `sdiff_symmDiff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:418:8: `symmDiff_symmDiff_self'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:588:8: `symmDiff_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:591:8: `bihimp_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/SymmDiff.lean:634:8: `symmDiff_symmDiff_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [461/493] Built Mathlib.Data.Set.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:127:9: `Set.PiSetCoe.canLift'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:153:8: `SetCoe.exists'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:157:8: `SetCoe.forall'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:391:8: `Set.nonempty_of_ssubset'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:1029:8: `Set.setOf_eq_eq_singleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:1208:8: `Set.eq_of_nonempty_of_subsingleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:1456:8: `Set.union_diff_cancel'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:2145:8: `Disjoint.inter_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Basic.lean:2151:8: `Disjoint.inter_right'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [464/493] Built Mathlib.Data.Set.Image
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:107:8: `Set.preimage_id'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:635:8: `Set.Nonempty.preimage'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:728:8: `Set.preimage_eq_preimage'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:755:8: `Set.range_id'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:847:8: `Set.range_quotient_mk'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:850:6: `Set.Quotient.range_mk''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:854:8: `Set.range_quotient_lift_on'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:920:8: `Set.range_ite_subset'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:1261:8: `Subtype.preimage_coe_compl'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Image.lean:1410:6: `sigma_mk_preimage_image'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [466/493] Built Mathlib.Order.Directed
warning: ././.lake/packages/mathlib/././Mathlib/Order/Directed.lean:68:8: `DirectedOn.mono'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Directed.lean:218:8: `directedOn_pair'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Directed.lean:287:18: `IsMin.not_isMax'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Order/Directed.lean:293:18: `IsMax.not_isMin'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [467/493] Built Mathlib.Data.Set.Prod
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Prod.lean:684:8: `Set.pi_eq_empty_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Prod.lean:703:8: `Set.singleton_pi'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Prod.lean:849:8: `Set.eval_preimage'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [468/493] Built Mathlib.Data.Set.Function
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:278:8: `Set.mapsTo'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:331:6: `Set.mapsTo_of_subsingleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:773:6: `Set.surjOn_of_subsingleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:920:6: `Set.bijOn_of_subsingleton'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:1026:8: `Set.LeftInvOn.image_inter'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:1042:8: `Set.LeftInvOn.image_image'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:1406:8: `Set.EqOn.piecewise_ite'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:1548:8: `Function.update_comp_eq_of_not_mem_range'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Function.lean:1642:6: `Equiv.bijOn'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [470/493] Built Mathlib.Data.Set.Pairwise.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Pairwise/Basic.lean:73:8: `Set.Pairwise.mono'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Set/Pairwise/Basic.lean:311:8: `Set.PairwiseDisjoint.elim'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [473/493] Built Mathlib.Data.List.Dedup
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Dedup.lean:33:8: `List.dedup_cons_of_mem'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/List/Dedup.lean:36:8: `List.dedup_cons_of_not_mem'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [474/493] Built Mathlib.Data.Multiset.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:66:8: `Multiset.quot_mk_to_coe'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:70:8: `Multiset.quot_mk_to_coe''` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:413:8: `Multiset.induction_on'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1170:8: `Multiset.map_id'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1178:16: `Multiset.map_const'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1308:8: `Multiset.foldr_induction'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1322:8: `Multiset.foldl_induction'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1395:8: `Multiset.attach_map_val'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:1879:6: `Multiset.map_filter'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:2260:8: `Multiset.ext'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:2311:8: `Multiset.filter_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Basic.lean:2586:6: `Multiset.filter_attach'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [477/493] Built Mathlib.Data.Multiset.Dedup
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Dedup.lean:56:8: `Multiset.dedup_subset'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Multiset/Dedup.lean:60:8: `Multiset.subset_dedup'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [478/493] Built Mathlib.Data.Finset.Defs
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Defs.lean:120:14: `Finset.forall_mem_not_eq'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Defs.lean:148:9: `Finset.decidableMem'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Defs.lean:182:9: `Finset.PiFinsetCoe.canLift'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Defs.lean:426:8: `Finset.pairwise_subtype_iff_pairwise_finset'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [484/493] Built Mathlib.Data.Finset.Filter
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Filter.lean:231:6: `Finset.filter_inj'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [486/493] Built Mathlib.Data.Finset.Insert
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Insert.lean:170:8: `Finset.subset_singleton_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Insert.lean:365:8: `Finset.insert_val'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Insert.lean:680:8: `Finset.pairwise_cons'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [490/493] Built Mathlib.Data.Finset.SDiff
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/SDiff.lean:182:6: `Finset.insert_sdiff_insert'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/SDiff.lean:213:8: `Finset.sdiff_sdiff_left'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [491/493] Built Mathlib.Data.Finset.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Basic.lean:195:8: `Finset.erase_injOn'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Basic.lean:350:8: `Finset.disjoint_filter_filter'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Data/Finset/Basic.lean:490:8: `Finset.filter_ne'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [492/493] Built BatteriesExtraLean.DFT
warning: ././././BatteriesExtraLean/DFT.lean:150:2: `List.join` has been deprecated: use `List.flatten` instead
warning: ././././BatteriesExtraLean/DFT.lean:224:21: `List.join` has been deprecated: use `List.flatten` instead
warning: ././././BatteriesExtraLean/DFT.lean:272:10: `Nat.pred_lt'` has been deprecated: use `Nat.pred_lt_of_lt` instead
info: ././././BatteriesExtraLean/DFT.lean:903:0: -- Found 0 errors in 56 declarations (plus 92 automatically generated ones) in the current file with 15 linters


-- All linting checks passed!
Build completed successfully.