Documentation
Batteries
Search
Google site search
return to top
source
Imports
Init
Batteries.CodeAction
Batteries.Linter
Batteries.Logic
Batteries.StdDeprecations
Batteries.WF
Batteries.Classes.Cast
Batteries.Classes.Order
Batteries.Classes.RatCast
Batteries.Classes.SatisfiesM
Batteries.CodeAction.Attr
Batteries.CodeAction.Basic
Batteries.CodeAction.Deprecated
Batteries.CodeAction.Misc
Batteries.Control.ForInStep
Batteries.Control.Lemmas
Batteries.Data.Array
Batteries.Data.AssocList
Batteries.Data.BinaryHeap
Batteries.Data.BinomialHeap
Batteries.Data.ByteArray
Batteries.Data.ByteSubarray
Batteries.Data.Char
Batteries.Data.DList
Batteries.Data.Fin
Batteries.Data.FloatArray
Batteries.Data.HashMap
Batteries.Data.LazyList
Batteries.Data.List
Batteries.Data.MLList
Batteries.Data.Nat
Batteries.Data.PairingHeap
Batteries.Data.RBMap
Batteries.Data.Range
Batteries.Data.Rat
Batteries.Data.String
Batteries.Data.UInt
Batteries.Data.UnionFind
Batteries.Data.Vector
Batteries.Lean.AttributeExtra
Batteries.Lean.Delaborator
Batteries.Lean.Except
Batteries.Lean.Expr
Batteries.Lean.Float
Batteries.Lean.HashMap
Batteries.Lean.HashSet
Batteries.Lean.Json
Batteries.Lean.MonadBacktrack
Batteries.Lean.NameMap
Batteries.Lean.NameMapAttribute
Batteries.Lean.PersistentHashMap
Batteries.Lean.PersistentHashSet
Batteries.Lean.Position
Batteries.Lean.Syntax
Batteries.Lean.TagAttribute
Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnreachableTactic
Batteries.Tactic.Alias
Batteries.Tactic.Basic
Batteries.Tactic.Case
Batteries.Tactic.Congr
Batteries.Tactic.Exact
Batteries.Tactic.HelpCmd
Batteries.Tactic.Init
Batteries.Tactic.Instances
Batteries.Tactic.Lemma
Batteries.Tactic.Lint
Batteries.Tactic.NoMatch
Batteries.Tactic.OpenPrivate
Batteries.Tactic.PermuteGoals
Batteries.Tactic.PrintDependents
Batteries.Tactic.PrintPrefix
Batteries.Tactic.SeqFocus
Batteries.Tactic.ShowUnused
Batteries.Tactic.SqueezeScope
Batteries.Tactic.Trans
Batteries.Tactic.Unreachable
Batteries.Tactic.Where
Batteries.Util.Cache
Batteries.Util.ExtendedBinder
Batteries.Util.LibraryNote
Batteries.Util.Panic
Batteries.Util.Pickle
Batteries.Util.ProofWanted
Batteries.Control.ForInStep.Basic
Batteries.Control.ForInStep.Lemmas
Batteries.Control.Nondet.Basic
Batteries.Lean.IO.Process
Batteries.Lean.Meta.Basic
Batteries.Lean.Meta.DiscrTree
Batteries.Lean.Meta.Expr
Batteries.Lean.Meta.Inaccessible
Batteries.Lean.Meta.InstantiateMVars
Batteries.Lean.Meta.SavedState
Batteries.Lean.Meta.Simp
Batteries.Lean.Meta.UnusedNames
Batteries.Lean.System.IO
Batteries.Lean.Util.EnvSearch
Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.Misc
Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.TypeClass
Batteries.Test.Internal.DummyLabelAttr
Batteries.Test.Internal.DummyLibraryNote
Batteries.Test.Internal.DummyLibraryNote2
Imported by