Documentation
Batteries
Search
Google site search
return to top
source
Imports
Init
Batteries.CodeAction
Batteries.Linter
Batteries.Logic
Batteries.StdDeprecations
Batteries.WF
Batteries.Classes.BEq
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.BitVec
Batteries.Data.Bool
Batteries.Data.ByteArray
Batteries.Data.Char
Batteries.Data.DList
Batteries.Data.Fin
Batteries.Data.HashMap
Batteries.Data.Int
Batteries.Data.LazyList
Batteries.Data.List
Batteries.Data.MLList
Batteries.Data.Nat
Batteries.Data.Option
Batteries.Data.PairingHeap
Batteries.Data.RBMap
Batteries.Data.Range
Batteries.Data.Rat
Batteries.Data.String
Batteries.Data.Sum
Batteries.Data.Thunk
Batteries.Data.UInt
Batteries.Data.UnionFind
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.Name
Batteries.Lean.NameMap
Batteries.Lean.NameMapAttribute
Batteries.Lean.PersistentHashMap
Batteries.Lean.PersistentHashSet
Batteries.Lean.Position
Batteries.Lean.SMap
Batteries.Lean.Syntax
Batteries.Lean.TagAttribute
Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnreachableTactic
Batteries.Tactic.Alias
Batteries.Tactic.Basic
Batteries.Tactic.Case
Batteries.Tactic.Classical
Batteries.Tactic.Congr
Batteries.Tactic.Exact
Batteries.Tactic.Init
Batteries.Tactic.Instances
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.Unreachable
Batteries.Tactic.Where
Batteries.Util.Cache
Batteries.Util.CheckTactic
Batteries.Util.ExtendedBinder
Batteries.Util.LibraryNote
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.AssertHypotheses
Batteries.Lean.Meta.Basic
Batteries.Lean.Meta.Clear
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.Lean.Util.Path
Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.Misc
Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.TypeClass
Batteries.Test.Internal.DummyLabelAttr
Imported by