Physlib Documentation
Batteries
Search
Google site search
return to top
source
Imports
Init
Batteries.CodeAction
Batteries.Linter
Batteries.Logic
Batteries.Classes.Cast
Batteries.Classes.Deprecated
Batteries.Classes.Order
Batteries.Classes.RatCast
Batteries.Classes.SatisfiesM
Batteries.CodeAction.Attr
Batteries.CodeAction.Basic
Batteries.CodeAction.Deprecated
Batteries.CodeAction.Match
Batteries.CodeAction.Misc
Batteries.Control.AlternativeMonad
Batteries.Control.ForInStep
Batteries.Control.LawfulMonadState
Batteries.Control.Lemmas
Batteries.Control.Monad
Batteries.Control.OptionT
Batteries.Data.Array
Batteries.Data.AssocList
Batteries.Data.BinaryHeap
Batteries.Data.BinomialHeap
Batteries.Data.BitVec
Batteries.Data.Bool
Batteries.Data.ByteArray
Batteries.Data.ByteSlice
Batteries.Data.Char
Batteries.Data.DList
Batteries.Data.Fin
Batteries.Data.FloatArray
Batteries.Data.HashMap
Batteries.Data.Int
Batteries.Data.List
Batteries.Data.MLList
Batteries.Data.NameSet
Batteries.Data.Nat
Batteries.Data.PairingHeap
Batteries.Data.RBMap
Batteries.Data.Random
Batteries.Data.Range
Batteries.Data.Rat
Batteries.Data.RunningStats
Batteries.Data.Stream
Batteries.Data.String
Batteries.Data.UInt
Batteries.Data.UnionFind
Batteries.Data.Vector
Batteries.Lean.AttributeExtra
Batteries.Lean.EStateM
Batteries.Lean.Except
Batteries.Lean.Expr
Batteries.Lean.Float
Batteries.Lean.HashMap
Batteries.Lean.HashSet
Batteries.Lean.Json
Batteries.Lean.LawfulMonad
Batteries.Lean.LawfulMonadLift
Batteries.Lean.MonadBacktrack
Batteries.Lean.NameMapAttribute
Batteries.Lean.PersistentHashMap
Batteries.Lean.PersistentHashSet
Batteries.Lean.Position
Batteries.Lean.SatisfiesM
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.GeneralizeProofs
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.PrintOpaques
Batteries.Tactic.PrintPrefix
Batteries.Tactic.SeqFocus
Batteries.Tactic.ShowUnused
Batteries.Tactic.SqueezeScope
Batteries.Tactic.Trans
Batteries.Tactic.Unreachable
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
Imported by