Documentation
Std
Search
Google site search
return to top
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.Array
Std.Data.AssocList
Std.Data.BinomialHeap
Std.Data.BitVec
Std.Data.Bool
Std.Data.ByteArray
Std.Data.Char
Std.Data.DList
Std.Data.Fin
Std.Data.HashMap
Std.Data.Int
Std.Data.Json
Std.Data.List
Std.Data.MLList
Std.Data.Nat
Std.Data.Option
Std.Data.Ord
Std.Data.PairingHeap
Std.Data.Prod
Std.Data.RBMap
Std.Data.Range
Std.Data.Rat
Std.Data.String
Std.Data.Sum
Std.Data.UInt
Std.Lean.AttributeExtra
Std.Lean.Command
Std.Lean.CoreM
Std.Lean.Delaborator
Std.Lean.Except
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.NameMap
Std.Lean.NameMapAttribute
Std.Lean.Parser
Std.Lean.PersistentHashMap
Std.Lean.PersistentHashSet
Std.Lean.Position
Std.Lean.SMap
Std.Lean.Syntax
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.Classical
Std.Tactic.CoeExt
Std.Tactic.Congr
Std.Tactic.Exact
Std.Tactic.Ext
Std.Tactic.FalseOrByContra
Std.Tactic.GuardExpr
Std.Tactic.GuardMsgs
Std.Tactic.HaveI
Std.Tactic.Init
Std.Tactic.Instances
Std.Tactic.LabelAttr
Std.Tactic.LeftRight
Std.Tactic.LibrarySearch
Std.Tactic.Lint
Std.Tactic.NoMatch
Std.Tactic.NormCast
Std.Tactic.Omega
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.SolveByElim
Std.Tactic.SqueezeScope
Std.Tactic.TryThis
Std.Tactic.Unreachable
Std.Tactic.Where
Std.Util.Cache
Std.Util.CheckTactic
Std.Util.ExtendedBinder
Std.Util.LibraryNote
Std.Util.Pickle
Std.Util.ProofWanted
Std.Util.TermUnsafe
Std.Control.ForInStep.Basic
Std.Control.ForInStep.Lemmas
Std.Control.Nondet.Basic
Std.Lean.Elab.Tactic
Std.Lean.IO.Process
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.LazyDiscrTree
Std.Lean.Meta.SavedState
Std.Lean.Meta.Simp
Std.Lean.Meta.UnusedNames
Std.Lean.System.IO
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.Omega.Config
Std.Tactic.Omega.Constraint
Std.Tactic.Omega.Core
Std.Tactic.Omega.Frontend
Std.Tactic.Omega.Int
Std.Tactic.Omega.IntList
Std.Tactic.Omega.LinearCombo
Std.Tactic.Omega.Logic
Std.Tactic.Omega.MinNatAbs
Std.Tactic.Omega.OmegaM
Std.Tactic.Relation.Rfl
Std.Tactic.Relation.Symm
Std.Tactic.SolveByElim.Backtrack
Std.Test.Internal.DummyLabelAttr
Std.Tactic.Omega.Coeffs.IntList
Imported by