Documentation
Init
Search
Google site search
return to top
source
Imports
Init.BinderPredicates
Init.ByCases
Init.Control
Init.Conv
Init.Core
Init.Data
Init.Dynamic
Init.Ext
Init.Grind
Init.Guard
Init.Hints
Init.MacroTrace
Init.Meta
Init.MetaTypes
Init.Notation
Init.NotationExtra
Init.Omega
Init.Prelude
Init.PropLemmas
Init.RCases
Init.ShareCommon
Init.SimpLemmas
Init.Simproc
Init.SizeOfLemmas
Init.System
Init.Tactics
Init.TacticsExtra
Init.Util
Init.WF
Init.WFTactics
Init.Data.Basic
Imported by
Std.Sat.AIG.RefVecOperator.Zip
Batteries.Lean.NameMapAttribute
Aesop.Options.Public
Aesop.RuleTac.Preprocess
Aesop.Rule
Aesop.Exception
Std.Sat.AIG.Lemmas
Std.Sat.AIG.Basic
ProofWidgets.Compat
Lake.Build.Fetch
Aesop.Rule.Basic
Aesop.BuiltinRules.Rfl
Batteries.CodeAction.Misc
Lake.Build.Common
Lake.Toml.Data.Dict
Aesop.RuleTac.Cases
Lake.DSL.Attributes
Lake.Util.List
Batteries.Tactic.Lint.Frontend
Aesop.Frontend.Attribute
Std.Sat.AIG.CNF
ImportGraph.Imports
Std.Sat.AIG.LawfulOperator
ModuleLocalProperties.MissingLemmas.FlatIff
Lake.Util.JsonObject
Batteries.Lean.Except
Aesop.Util.UnorderedArraySet
Lake.Config.Module
Lake.Toml.Data.DateTime
Lake.Config.Workspace
Aesop.Script.Check
Batteries.Data.Rat.Lemmas
ModuleLocalProperties.MissingLemmas.TensorProduct
Batteries.Lean.NameMap
Aesop.Search.SearchM
Aesop.Builder.Cases
Aesop.Search.RuleSelection
Aesop.Tree.Free
Aesop.Script.StructureStatic
Aesop.Builder.Basic
Lake.Config.ExternLib
ModuleLocalProperties.Flat
Lake.Util.StoreInsts
Aesop.RuleTac
Batteries.Linter.UnreachableTactic
Lake.DSL.Extensions
Lake.Config.InstallPath
Batteries.Tactic.Unreachable
Batteries.Data.List.Perm
Aesop.BuiltinRules.Intros
Aesop.Percent
Batteries.Lean.AttributeExtra
Lake.Util.Version
Aesop.Search.Expansion.Simp
Batteries.Data.List.Basic
Lake.Util.Task
Lake
Lake.Build.Imports
Batteries.Logic
Aesop.Frontend.Command
ModuleLocalProperties.Basic
Lake.Config
Batteries.Tactic.Basic
Batteries.Data.BinomialHeap.Basic
Batteries.Linter
Aesop.Script.OptimizeSyntax
Batteries.Data.Sum.Basic
Batteries.Data.RBMap.WF
Lake.Util.Lock
Lake.DSL.Script
Lake.Build.Store
Aesop.Index
Aesop.Search.ExpandSafePrefix
Aesop.Stats.Extension
Aesop.Tree.Traversal
Batteries.Tactic.PermuteGoals
Batteries.WF
ProofWidgets.Component.MakeEditLink
ProofWidgets.Cancellable
Aesop.RuleTac.Apply
Lake.Config.Script
Aesop.Tree.ExtractProof
Batteries.Data.List.Lemmas
Lake.Toml.Elab
Batteries.Data.List.OfFn
Lake.DSL.Require
ModuleLocalProperties.SpanIsom
Lake.Config.Opaque
Aesop.Main
Qq.MetaM
Lake.Config.Package
Aesop.Tree.AddRapp
Aesop.Stats.Basic
Lake.Util.Message
Lake.Build.Module
Aesop.Frontend.Tactic
Aesop.Index.Basic
Aesop.RuleTac.Forward
Aesop.Rule.Name
Batteries.Lean.Syntax
Batteries.Data.Nat.Gcd
Lake.Build.Facets
Lake.Build.Library
Std.Sat.AIG.CachedGatesLemmas
Batteries.Tactic.Lint.Misc
Lake.Util.Family
Std.Sat.AIG.RefVecOperator
Batteries.Data.List.Count
Aesop.Util.Tactic.Ext
Batteries.Tactic.Init
Batteries.Data.RBMap.Alter
Qq.Match
Batteries.Data.Array.Init.Lemmas
Lake.Toml.Data.Value
LeanSearchClient
Lake.Build.Data
Std.Sat.AIG.RefVecOperator.Map
Batteries.Lean.Float
Aesop.Util.Tactic
Lake.Toml.ParserUtil
Qq.ForLean.Do
Batteries.Tactic.Lint.Basic
Aesop.RuleSet.Name
Batteries.Lean.Position
Batteries.Data.Fin.Basic
Qq.SortLocalDecls
Batteries.Tactic.Lint.TypeClass
Batteries.CodeAction
Lake.Config.ExternLibConfig
Lake.CLI.Actions
Batteries.Lean.Meta.Basic
Aesop.RuleTac.FVarIdSubst
Std.Sat.AIG.Cached
Aesop.BuiltinRules.DestructProducts
Lake.Config.TargetConfig
Batteries.CodeAction.Attr
Aesop.Search.Queue.Class
Lake.DSL.Package
ProofWidgets.Component.Basic
Aesop.Util.Tactic.Unfold
Aesop.Builder.Apply
Qq.Typ
Lake.Util.Opaque
Std.Sat.AIG.Relabel
Aesop.Tree
Batteries.Tactic.Classical
Lake.Config.Context
Batteries.Classes.RatCast
ProofWidgets.Util
Aesop.Builder.Forward
Std.Sat.AIG.RefVecOperator.Fold
Aesop.Util.UnionFind
Batteries.Data.List.Pairwise
Aesop.RulePattern
Lake.Build.Key
Aesop.Tree.RunMetaM
Aesop.Builder.Tactic
Aesop.Search.Expansion
Lake.Config.LeanLib
Batteries.Tactic.SeqFocus
Lake.Util.FilePath
Batteries.Util.LibraryNote
ProofWidgets.Component.OfRpcMethod
Batteries.Classes.Order
Aesop.Util.EqualUpToIds
Lake.Build.Basic
Lake.Build.Package
Batteries.Linter.UnnecessarySeqFocus
Batteries.Data.RBMap.Basic
Lake.Build.Job
Lake.Util.Casing
Aesop.Script.SScript
Batteries.Lean.Meta.DiscrTree
Aesop.Tree.Check
Lake.DSL.AttributesCore
Qq.AssertInstancesCommute
Lake.DSL.Meta
ModuleLocalProperties
Lake.DSL.DeclUtil
Batteries.Tactic.Exact
Lake.Build.Info
Lake.Toml.Load
Aesop.Frontend.Basic
Lake.Util.Exit
Lake.Util.Cycle
Aesop.Script.TacticState
Lake.Config.LeanExeConfig
Lake.Util.OrdHashSet
Batteries.Tactic.Congr
Batteries.Tactic.OpenPrivate
Lake.Load.Config
Lake.Toml.Grammar
Std.Sat.AIG.RelabelNat
Aesop.Tree.UnsafeQueue
Batteries.Lean.HashSet
Lake.Build.Run
Batteries.Data.List.Init.Lemmas
Batteries.Data.String.Basic
Aesop.RuleTac.GoalDiff
Lake.Config.Dependency
Std.Sat.AIG.CachedLemmas
Lake.Config.LeanConfig
Aesop.Frontend.RuleExpr
Batteries.Tactic.Where
ModuleLocalProperties.MissingLemmas.LocalizaedIsTensorProduct
Batteries.CodeAction.Basic
Aesop.BuiltinRules.Ext
Aesop.Script.ScriptM
Aesop.Script.StructureDynamic
Batteries.Lean.Meta.UnusedNames
Lake.Build.Topological
Aesop.Script.CtorNames
Lake.Build.Trace
Lake.Build.Executable
Lake.Config.Defaults
Batteries.Lean.MonadBacktrack
ModuleLocalProperties.Isom
Aesop.Options
Aesop.Util.Basic
Aesop.Search.Main
Aesop.BuiltinRules.Split
Aesop.Script.Tactic
Aesop.Script.GoalWithMVars
Aesop.Builder.Default
Lake.Util.IO
Std.Sat.AIG.CachedGates
Aesop.RuleSet
Aesop.Tree.ExtractScript
Lake.Util.OrderedTagAttribute
Lake.Toml
LeanSearchClient.LoogleSyntax
Lake.Version
Lake.Toml.Elab.Expression
Aesop.BuiltinRules.Assumption
Aesop.Frontend.Extension.Init
Batteries.Util.ProofWanted
Lake.Config.Env
Batteries.Lean.Meta.InstantiateMVars
Lake.Toml.Elab.Value
Lake.Build.Actions
Lake.Config.WorkspaceConfig
Lake.Config.FacetConfig
Aesop
Aesop.Script.Util
Batteries.Lean.Meta.Inaccessible
Aesop.Saturate
Batteries.Control.ForInStep.Basic
Aesop.Builder.NormSimp
Batteries.Tactic.Alias
Lake.Util.EquipT
Lake.DSL
Batteries.Data.Array.Merge
Batteries.Tactic.Trans
Aesop.Script.UScriptToSScript
ModuleLocalProperties.MissingLemmas.Range
ModuleLocalProperties.MissingLemmas.Units
Aesop.Script.SpecificTactics
Lake.Util.Lift
Aesop.ElabM
Batteries.Tactic.Lint.Simp
Batteries.Data.Fin.Lemmas
Lake.Util.Log
Aesop.Constants
Lake.Util.EStateT
Aesop.Tree.Tracing
Aesop.Script.UScript
Batteries.Data.Rat.Basic
Aesop.Script.Step
Lake.Util.Proc
Aesop.BuiltinRules.ApplyHyps
Qq.Delab
Aesop.Options.Internal
Aesop.RuleTac.Forward.Basic
Lake.Util.Store
Batteries.Util.Cache
Lake.Util.Error
Lake.Util.Sugar
Aesop.Frontend.Extension
Lean
Std.Sat.AIG.If
ModuleLocalProperties.FinitePresentation
Qq.ForLean.ReduceEval
Lake.Build.Targets
Batteries.Data.Sum.Lemmas
Lake.Config.Glob
Qq.Macro
Std.Sat.AIG.RefVec
Aesop.Search.Queue
ModuleLocalProperties.Defs
Lake.CLI.Build
ModuleLocalProperties.MissingLemmas.Submodule
Batteries.Lean.PersistentHashMap
Aesop.Tree.TreeM
Aesop.Stats.Report
Lake.Util.Binder
Lake.CLI.Error
Lake.DSL.Config
Lake.Config.Monad
Aesop.Tree.State
Lake.Util.DRBMap
Aesop.BuiltinRules
Aesop.RuleTac.Tactic
Lake.Util.Git
LeanSearchClient.Syntax
Aesop.RuleTac.ElabRuleTerm
Batteries.Lean.TagAttribute
Batteries.Data.MLList.Basic
Batteries.Lean.Meta.Expr
Lake.Reservoir
Aesop.Search.Expansion.Basic
Lake.Build.Index
Batteries.Control.Nondet.Basic
Lake.DSL.Targets
Aesop.Frontend.Saturate
Batteries.Control.ForInStep.Lemmas
Aesop.Builder.Constructors
Aesop.Script.Main
Lake.Config.LeanLibConfig
ModuleLocalProperties.MissingLemmas.LocalizedModule
Aesop.RuleSet.Member
Qq
Aesop.Check
Qq.ForLean.ToExpr
Lake.Util.RBArray
Aesop.Nanos
Batteries.Lean.Expr
Std.Sat.AIG.LawfulVecOperator
Aesop.RuleSet.Filter
Lake.Util.Name
Lake.Util.NativeLib
Batteries.Tactic.Lint
Batteries.CodeAction.Deprecated
Lake.Config.LeanExe
Aesop.Tree.Data
ImportGraph.RequiredModules
Aesop.BuiltinRules.Subst
Aesop.RuleTac.Basic
Lake.Util.Compare
LeanSearchClient.Basic
Batteries.Lean.PersistentHashSet
Batteries.Lean.Meta.SavedState
Aesop.Search.Expansion.Norm
Batteries.Data.Array.Basic
Batteries.Data.Nat.Basic
Batteries.Util.ExtendedBinder
ProofWidgets.Data.Html
Aesop.Tracing
Lake.Build
Std.Sat.AIG
Aesop.Builder.Unfold