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.Data.AssocList
Std.Data.BinomialHeap
Std.Data.Char
Std.Data.DList
Std.Data.HashMap
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.Format
Std.Lean.HashMap
Std.Lean.HashSet
Std.Lean.InfoTree
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.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.Lint
Std.Tactic.NoMatch
Std.Tactic.OpenPrivate
Std.Tactic.PrintDependents
Std.Tactic.RCases
Std.Tactic.Replace
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.ExtendedBinder
Std.Util.LibraryNote
Std.Util.Pickle
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.Fin.Basic
Std.Data.Fin.Lemmas
Std.Data.HashMap.Basic
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.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.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.LCtx
Std.Lean.Meta.SavedState
Std.Lean.Meta.UnusedNames
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.Test.Internal.DummyLabelAttr
Std.Data.Array.Init.Basic
Std.Data.Array.Init.Lemmas
Std.Data.List.Init.Lemmas
Std.Data.Nat.Init.Lemmas
Std.Data.Option.Init.Lemmas
Imported by