Documentation Verification Report

Modules

165 modules

ModuleDefinitionsTheoremsSorry
Batteries/Classes/Cast.lean 1 0
Batteries/Classes/Deprecated.lean 12 55
Batteries/Classes/Order.lean 10 55
Batteries/Classes/RatCast.lean 6 0
Batteries/Classes/SatisfiesM.lean 9 25
Batteries/CodeAction/Attr.lean 18 0
Batteries/CodeAction/Basic.lean 1 0
Batteries/CodeAction/Deprecated.lean 2 0
Batteries/CodeAction/Match.lean 6 0
Batteries/CodeAction/Misc.lean 13 0
Batteries/Control/AlternativeMonad.lean 11 23
Batteries/Control/ForInStep/Basic.lean 4 0
Batteries/Control/ForInStep/Lemmas.lean 0 11
Batteries/Control/LawfulMonadState.lean 1 47
Batteries/Control/Lemmas.lean 0 12
Batteries/Control/Monad.lean 0 2
Batteries/Control/Nondet/Basic.lean 27 0
Batteries/Control/OptionT.lean 0 3
Batteries/Data/Array/Basic.lean 23 0
Batteries/Data/Array/Lemmas.lean 0 15
Batteries/Data/Array/Match.lean 19 2
Batteries/Data/Array/Merge.lean 11 0
Batteries/Data/Array/Monadic.lean 0 12
Batteries/Data/Array/Pairwise.lean 2 8
Batteries/Data/Array/Scan.lean 0 61
Batteries/Data/AssocList.lean 32 36
Batteries/Data/BinaryHeap.lean 1 0
Batteries/Data/BinaryHeap/Basic.lean 21 3
Batteries/Data/BinomialHeap.lean 1 0
Batteries/Data/BinomialHeap/Basic.lean 70 22
Batteries/Data/BinomialHeap/Lemmas.lean 0 4
Batteries/Data/BitVec/Basic.lean 3 0
Batteries/Data/BitVec/Lemmas.lean 0 27
Batteries/Data/Bool.lean 2 0
Batteries/Data/ByteArray.lean 6 21
Batteries/Data/ByteSlice.lean 28 4
Batteries/Data/Char/AsciiCasing.lean 4 17
Batteries/Data/Char/Basic.lean 8 16
Batteries/Data/DList.lean 1 0
Batteries/Data/DList/Basic.lean 13 1
Batteries/Data/DList/Lemmas.lean 0 9
Batteries/Data/Fin/Basic.lean 17 0
Batteries/Data/Fin/Fold.lean 0 24
Batteries/Data/Fin/Lemmas.lean 0 107
Batteries/Data/Fin/OfBits.lean 1 1
Batteries/Data/FloatArray.lean 4 0
Batteries/Data/HashMap/Basic.lean 30 0
Batteries/Data/Int.lean 2 4
Batteries/Data/List/ArrayMap.lean 1 2
Batteries/Data/List/Basic.lean 129 27
Batteries/Data/List/Count.lean 2 16
Batteries/Data/List/Lemmas.lean 0 305
Batteries/Data/List/Matcher.lean 11 0
Batteries/Data/List/Monadic.lean 0 2
Batteries/Data/List/Pairwise.lean 0 11
Batteries/Data/List/Perm.lean 4 72
Batteries/Data/List/Scan.lean 0 77
Batteries/Data/MLList/Basic.lean 68 0
Batteries/Data/MLList/Heartbeats.lean 1 0
Batteries/Data/MLList/IO.lean 1 0
Batteries/Data/NameSet.lean 4 0
Batteries/Data/Nat/Basic.lean 12 1
Batteries/Data/Nat/Bisect.lean 2 13
Batteries/Data/Nat/Bitwise.lean 0 23
Batteries/Data/Nat/Digits.lean 0 5
Batteries/Data/Nat/Gcd.lean 0 1
Batteries/Data/Nat/Lemmas.lean 2 33
Batteries/Data/PairingHeap.lean 45 21
Batteries/Data/RBMap.lean 1 0
Batteries/Data/RBMap/Alter.lean 9 25
Batteries/Data/RBMap/Basic.lean 205 7
Batteries/Data/RBMap/Depth.lean 3 8
Batteries/Data/RBMap/Lemmas.lean 11 237
Batteries/Data/RBMap/WF.lean 11 67
Batteries/Data/Random/MersenneTwister.lean 20 2
Batteries/Data/Range/Lemmas.lean 0 2
Batteries/Data/Rat/Float.lean 4 0
Batteries/Data/RunningStats.lean 8 0
Batteries/Data/Stream.lean 7 10
Batteries/Data/String/Basic.lean 4 0
Batteries/Data/String/Legacy.lean 29 0
Batteries/Data/String/Lemmas.lean 7 211
Batteries/Data/String/Matcher.lean 19 0
Batteries/Data/UInt.lean 0 59
Batteries/Data/UnionFind.lean 1 0
Batteries/Data/UnionFind/Basic.lean 38 43
Batteries/Data/UnionFind/Lemmas.lean 0 24
Batteries/Data/Vector/Basic.lean 1 0
Batteries/Data/Vector/Lemmas.lean 0 23
Batteries/Data/Vector/Monadic.lean 0 3
Batteries/Lean/AttributeExtra.lean 16 0
Batteries/Lean/EStateM.lean 1 36
Batteries/Lean/Except.lean 2 8
Batteries/Lean/Expr.lean 14 0
Batteries/Lean/Float.lean 8 0
Batteries/Lean/HashMap.lean 3 0
Batteries/Lean/HashSet.lean 3 0
Batteries/Lean/IO/Process.lean 2 0
Batteries/Lean/Json.lean 3 0
Batteries/Lean/LawfulMonad.lean 0 10
Batteries/Lean/LawfulMonadLift.lean 0 8
Batteries/Lean/Meta/Basic.lean 16 0
Batteries/Lean/Meta/DiscrTree.lean 5 0
Batteries/Lean/Meta/Expr.lean 1 0
Batteries/Lean/Meta/Inaccessible.lean 3 0
Batteries/Lean/Meta/InstantiateMVars.lean 4 0
Batteries/Lean/Meta/SavedState.lean 4 0
Batteries/Lean/Meta/Simp.lean 4 0
Batteries/Lean/Meta/UnusedNames.lean 7 0
Batteries/Lean/MonadBacktrack.lean 1 0
Batteries/Lean/NameMapAttribute.lean 14 0
Batteries/Lean/PersistentHashMap.lean 6 0
Batteries/Lean/PersistentHashSet.lean 10 0
Batteries/Lean/Position.lean 3 0
Batteries/Lean/SatisfiesM.lean 1 0
Batteries/Lean/Syntax.lean 1 0
Batteries/Lean/System/IO.lean 1 0
Batteries/Lean/TagAttribute.lean 2 0
Batteries/Lean/Util/EnvSearch.lean 1 0
Batteries/Linter.lean 1 0
Batteries/Linter/UnnecessarySeqFocus.lean 13 0
Batteries/Linter/UnreachableTactic.lean 10 0
Batteries/Logic.lean 1 28
Batteries/Tactic/Alias.lean 11 0
Batteries/Tactic/Case.lean 9 0
Batteries/Tactic/Congr.lean 8 0
Batteries/Tactic/Exact.lean 2 0
Batteries/Tactic/GeneralizeProofs.lean 32 0
Batteries/Tactic/HelpCmd.lean 9 0
Batteries/Tactic/Init.lean 11 0
Batteries/Tactic/Instances.lean 2 0
Batteries/Tactic/Lemma.lean 4 0
Batteries/Tactic/Lint/Basic.lean 15 0
Batteries/Tactic/Lint/Frontend.lean 21 0
Batteries/Tactic/Lint/Misc.lean 11 0
Batteries/Tactic/Lint/Simp.lean 16 0
Batteries/Tactic/Lint/TypeClass.lean 2 0
Batteries/Tactic/NoMatch.lean 5 0
Batteries/Tactic/OpenPrivate.lean 9 0
Batteries/Tactic/PermuteGoals.lean 4 0
Batteries/Tactic/PrintDependents.lean 7 0
Batteries/Tactic/PrintOpaques.lean 6 0
Batteries/Tactic/PrintPrefix.lean 8 0
Batteries/Tactic/SeqFocus.lean 1 0
Batteries/Tactic/ShowUnused.lean 1 0
Batteries/Tactic/SqueezeScope.lean 2 0
Batteries/Tactic/Trans.lean 9 0
Batteries/Tactic/Unreachable.lean 2 0
Batteries/Util/Cache.lean 13 2
Batteries/Util/ExtendedBinder.lean 6 0
Batteries/Util/LibraryNote.lean 10 0
Batteries/Util/Panic.lean 1 1
Batteries/Util/Pickle.lean 3 0
Batteries/Util/ProofWanted.lean 1 0
BatteriesTest/MLList.lean 1 0
BatteriesTest/alias.lean 1 0
BatteriesTest/array.lean 1 0
BatteriesTest/congr.lean 0 2
BatteriesTest/openPrivate.lean 1 0
BatteriesTest/proof_wanted.lean 1 0
BatteriesTest/rfl.lean 0 1
BatteriesTest/satisfying.lean 1 0
BatteriesTest/seq_focus.lean 1 0
BatteriesTest/trans.lean 0 3
BatteriesTest/vector.lean 1 0