Documentation
Std
Search
Google site search
Std
source
Imports
Init
Std.CodeAction
Std.Linter
Std.Logic
Std.WF
Std.Classes.BEq
Std.Classes.Cast
Std.Classes.Dvd
Std.Classes.LawfulMonad
Std.Classes.Order
Std.Classes.RatCast
Std.Classes.SetNotation
Std.CodeAction.Attr
Std.CodeAction.Basic
Std.CodeAction.Deprecated
Std.CodeAction.Misc
Std.Control.ForInStep
Std.Control.Lemmas
Std.Data.AssocList
Std.Data.BinomialHeap
Std.Data.BitVec
Std.Data.Bool
Std.Data.Char
Std.Data.DList
Std.Data.HashMap
Std.Data.Json
Std.Data.Ord
Std.Data.PairingHeap
Std.Data.RBMap
Std.Data.Rat
Std.Data.String
Std.Data.Sum
Std.Lean.AttributeExtra
Std.Lean.Command
Std.Lean.CoreM
Std.Lean.Delaborator
Std.Lean.Expr
Std.Lean.Float
Std.Lean.Format
Std.Lean.HashMap
Std.Lean.HashSet
Std.Lean.InfoTree
Std.Lean.Json
Std.Lean.LocalContext
Std.Lean.MonadBacktrack
Std.Lean.Name
Std.Lean.NameMapAttribute
Std.Lean.Parser
Std.Lean.PersistentHashMap
Std.Lean.PersistentHashSet
Std.Lean.Position
Std.Lean.Tactic
Std.Lean.TagAttribute
Std.Linter.UnnecessarySeqFocus
Std.Linter.UnreachableTactic
Std.Tactic.Alias
Std.Tactic.Basic
Std.Tactic.ByCases
Std.Tactic.Case
Std.Tactic.Change
Std.Tactic.CoeExt
Std.Tactic.Congr
Std.Tactic.Exact
Std.Tactic.Ext
Std.Tactic.GuardExpr
Std.Tactic.GuardMsgs
Std.Tactic.HaveI
Std.Tactic.Instances
Std.Tactic.LabelAttr
Std.Tactic.LeftRight
Std.Tactic.Lint
Std.Tactic.NoMatch
Std.Tactic.NormCast
Std.Tactic.OpenPrivate
Std.Tactic.PermuteGoals
Std.Tactic.PrintDependents
Std.Tactic.PrintPrefix
Std.Tactic.RCases
Std.Tactic.Replace
Std.Tactic.RunCmd
Std.Tactic.SeqFocus
Std.Tactic.ShowTerm
Std.Tactic.SimpTrace
Std.Tactic.Simpa
Std.Tactic.SqueezeScope
Std.Tactic.TryThis
Std.Tactic.Unreachable
Std.Tactic.Where
Std.Util.Cache
Std.Util.ExtendedBinder
Std.Util.LibraryNote
Std.Util.Pickle
Std.Util.ProofWanted
Std.Util.TermUnsafe
Std.Control.ForInStep.Basic
Std.Control.ForInStep.Lemmas
Std.Data.Array.Basic
Std.Data.Array.Lemmas
Std.Data.Array.Match
Std.Data.Array.Merge
Std.Data.BinomialHeap.Basic
Std.Data.BinomialHeap.Lemmas
Std.Data.BitVec.Basic
Std.Data.BitVec.Bitblast
Std.Data.BitVec.Folds
Std.Data.BitVec.Lemmas
Std.Data.Fin.Basic
Std.Data.Fin.Iterate
Std.Data.Fin.Lemmas
Std.Data.HashMap.Basic
Std.Data.HashMap.Lemmas
Std.Data.HashMap.WF
Std.Data.Int.Basic
Std.Data.Int.DivMod
Std.Data.Int.Lemmas
Std.Data.List.Basic
Std.Data.List.Count
Std.Data.List.Lemmas
Std.Data.List.Pairwise
Std.Data.MLList.Basic
Std.Data.MLList.Heartbeats
Std.Data.Nat.Basic
Std.Data.Nat.Bitwise
Std.Data.Nat.Gcd
Std.Data.Nat.Lemmas
Std.Data.Option.Basic
Std.Data.Option.Lemmas
Std.Data.Prod.Lex
Std.Data.RBMap.Alter
Std.Data.RBMap.Basic
Std.Data.RBMap.Lemmas
Std.Data.RBMap.WF
Std.Data.Range.Lemmas
Std.Data.Rat.Basic
Std.Data.Rat.Lemmas
Std.Data.String.Basic
Std.Data.String.Lemmas
Std.Data.Sum.Basic
Std.Data.Sum.Lemmas
Std.Lean.Elab.Tactic
Std.Lean.Meta.AssertHypotheses
Std.Lean.Meta.Basic
Std.Lean.Meta.Clear
Std.Lean.Meta.DiscrTree
Std.Lean.Meta.Expr
Std.Lean.Meta.Inaccessible
Std.Lean.Meta.InstantiateMVars
Std.Lean.Meta.SavedState
Std.Lean.Meta.Simp
Std.Lean.Meta.UnusedNames
Std.Lean.Util.EnvSearch
Std.Lean.Util.Path
Std.Tactic.Ext.Attr
Std.Tactic.Lint.Basic
Std.Tactic.Lint.Frontend
Std.Tactic.Lint.Misc
Std.Tactic.Lint.Simp
Std.Tactic.Lint.TypeClass
Std.Tactic.NormCast.Ext
Std.Tactic.NormCast.Lemmas
Std.Tactic.Relation.Rfl
Std.Tactic.Relation.Symm
Std.Test.Internal.DummyLabelAttr
Std.Data.Array.Init.Basic
Std.Data.Array.Init.Lemmas
Std.Data.Fin.Init.Lemmas
Std.Data.List.Init.Attach
Std.Data.List.Init.Lemmas
Std.Data.Nat.Init.Lemmas
Std.Data.Option.Init.Lemmas
Imported by