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.While
Init.Data.Basic
Imported by
Lake.Util.Log
Lake.Util.Message
Batteries.Tactic.Alias
Aesop.Tree.Tracing
ProofWidgets.Cancellable
Aesop.Builder.Tactic
Lake.Config.InstallPath
Acmoi.Exercise1_10
Batteries.Tactic.Lint.Frontend
Lake.DSL.Extensions
Batteries.Lean.Except
Batteries.Data.List.Lemmas
Lake.Util.Lock
Aesop.Script.UScript
Aesop.Frontend.Basic
Batteries.Tactic.Lint
Lake.Build.Trace
Lake.Util.OrdHashSet
Aesop.Tree.ExtractScript
Batteries.Lean.HashMap
Lake.Config.Script
Batteries.WF
Aesop.Script.SScript
LeanSearchClient.LoogleSyntax
Aesop.RuleTac.Apply
Batteries.Data.String.Matcher
Batteries.Data.List.Perm
Aesop.Stats.Report
Batteries.Data.List.Init.Lemmas
Lake.Util.Casing
Lake.Build.Actions
Qq.ForLean.Do
Lake.Build.Data
Aesop.Builder.Forward
Acmoi.Exercise2_3
Aesop.Script.Check
Acmoi.Exercise1_4
ProofWidgets.Compat
Aesop.RuleTac.Cases
Batteries.Data.RBMap.Alter
Aesop.Util.UnorderedArraySet
Batteries.Lean.PersistentHashSet
Aesop.Script.OptimizeSyntax
Lake.Config.Env
Lake.Config.FacetConfig
Lake.Util.Version
Lake.Reservoir
Batteries.Data.Fin.Lemmas
Aesop.Builder.NormSimp
Batteries.Lean.Meta.InstantiateMVars
Lake.Config.Module
Lake.Build.Executable
Batteries.Tactic.SeqFocus
Aesop.Script.Tactic
Batteries.Classes.Order
Lake.Config.LeanConfig
Acmoi.Lemma9Singapore
Acmoi.TestingDimensionBound
Aesop.BuiltinRules.Split
ImportGraph.RequiredModules
Batteries.Data.RBMap.WF
Lake.DSL.DeclUtil
Lake.CLI.Actions
Qq.Match
Acmoi.Exercise2_4
Aesop.Builder.Default
Batteries.Lean.Expr
Aesop.Exception
Aesop.Tree.UnsafeQueue
Aesop.Stats.Basic
Lake
Acmoi.Exercise1_14
Aesop.Options.Public
Lake.Util.Name
Batteries.Data.MLList.Basic
Acmoi.Exercise4_2
Aesop.RuleSet.Filter
Aesop.Script.StructureDynamic
Aesop.Script.TacticState
Lake.Util.Sugar
Aesop.RuleSet.Member
Lake.Util.EStateT
Aesop.Stats.Extension
Batteries.Logic
Batteries.Data.RBMap.Basic
Batteries.Lean.AttributeExtra
Qq.Typ
Batteries.Lean.Meta.SavedState
Aesop.Util.EqualUpToIds
Aesop.Util.Basic
Lake.Toml.Elab.Expression
Acmoi.Theorem1_49
Batteries.Control.Nondet.Basic
Aesop.Frontend.Attribute
Lake.Util.Git
Lake.Toml.Elab
Aesop.Index
Lake.Toml
Aesop.Util.UnionFind
Lake.Build.Index
Aesop.Script.Util
Lake.Util.Lift
Lake.DSL.Attributes
Acmoi.Exercise3_1_2
Acmoi.Exercise3_3_4
Lake.Build.Package
Acmoi.Exercise1_11
Acmoi.Exercise1_3
ProofWidgets.Presentation.Expr
Batteries.Lean.Meta.Inaccessible
Lake.DSL.Package
Qq.AssertInstancesCommute
Aesop.Frontend.Command
Aesop.RuleTac.Forward.Basic
Qq.Delab
Batteries.Lean.Position
Lake.Toml.Data.DateTime
Batteries.Control.ForInStep.Lemmas
ProofWidgets.Util
ImportGraph.Imports
Lake.Config.Dependency
Lake.Config.LeanLib
Lake.CLI.Error
Lake.Config.Workspace
Aesop.BuiltinRules
Lake.Version
Lake.Util.IO
Lake.Util.Exit
Lake.Build.Module
Lake.Config.ExternLib
Lake.Config.ExternLibConfig
Lake.DSL
Acmoi.HydeTheorem
Lake.Build.Common
Lake.Toml.Load
Aesop.Builder.Basic
Lake.Util.OrderedTagAttribute
Batteries.Tactic.HelpCmd
Lake.DSL.AttributesCore
Batteries.Data.List.Basic
Acmoi.Exercise2_2
Lake.Config.LeanLibConfig
Batteries.Data.Array.Match
Lean
Lake.Toml.Data.Dict
Batteries.Lean.TagAttribute
Batteries.Linter.UnreachableTactic
Aesop.Search.Queue
Lake.Util.Family
Aesop.Util.Tactic
Batteries.CodeAction
Batteries.Data.Array.Merge
Batteries.Tactic.Congr
Aesop.Search.Main
Aesop.RuleTac.Tactic
Batteries.Data.Array.Basic
Batteries.Data.List.OfFn
Lake.Util.Opaque
Lake.Toml.Grammar
Lake.Toml.Data.Value
Aesop.Frontend.RuleExpr
Aesop.Search.ExpandSafePrefix
Aesop.BuiltinRules.DestructProducts
Batteries.Tactic.OpenPrivate
Lake.Config.Context
Aesop.Search.Expansion
Aesop.Util.Tactic.Unfold
Lake.Util.FilePath
Lake.Util.JsonObject
ProofWidgets.Component.Basic
Aesop.Constants
Batteries.Control.ForInStep.Basic
Batteries.Data.Fin.Basic
Batteries.Lean.NameMapAttribute
Aesop.Tree.ExtractProof
Aesop.Search.Queue.Class
Lake.Build.Key
Aesop.RuleTac
Qq.ForLean.ReduceEval
Batteries.CodeAction.Attr
Aesop.Search.SearchM
Aesop.Script.ScriptM
Aesop.BuiltinRules.Ext
Lake.Config.LeanExe
Batteries.Lean.Meta.Basic
Batteries.Lean.HashSet
Batteries.Linter
Aesop.Tree
Batteries.Lean.Meta.Expr
Aesop.Options.Internal
Aesop.BuiltinRules.Assumption
Acmoi.Exercise1_5
Batteries.Tactic.Exact
Lake.Util.EquipT
Batteries.Tactic.Trans
Batteries.Lean.Syntax
Batteries.Tactic.Lint.TypeClass
Batteries.Data.MLList.Heartbeats
Aesop.RuleTac.Basic
Lake.Util.Store
Aesop.Rule
LeanSearchClient.Syntax
Batteries.Data.List.Pairwise
Aesop.Rule.Basic
Acmoi.QuasTheorem
Lake.Build
Aesop.Tree.Traversal
Acmoi.Exercise1_8
Lake.Build.Imports
Aesop.BuiltinRules.Rfl
ProofWidgets.Component.HtmlDisplay
Lake.Build.Basic
Aesop.Rule.Name
Lake.Config.WorkspaceConfig
Acmoi.Exercise4_3
Aesop.Percent
Aesop.Main
Aesop.Nanos
Lake.Util.RBArray
Batteries.Tactic.Basic
Aesop.Frontend.Saturate
ProofWidgets.Component.MakeEditLink
Lake.Util.Error
Aesop.Tree.AddRapp
Lake.Config.Glob
Aesop.Script.Main
Acmoi.Exercise5_1
Qq.MetaM
Lake.Config.TargetConfig
Lake.Config.Monad
Aesop.Builder.Unfold
Lake.Util.Compare
Batteries.Tactic.Lint.Misc
Acmoi.Exercise2_1
Lake.Util.DRBMap
Aesop.Tree.Check
Lake.Config
Batteries.CodeAction.Misc
Aesop.Script.CtorNames
Lake.Util.StoreInsts
Lake.Build.Topological
Batteries.Util.ProofWanted
Aesop.Options
Lake.Util.NativeLib
Aesop.Script.UScriptToSScript
Batteries.Data.Nat.Basic
Batteries.Lean.Meta.UnusedNames
Aesop.Tree.Free
Aesop.RuleTac.ElabRuleTerm
Lake.Toml.Elab.Value
Aesop.Frontend.Extension
Acmoi.Exercise1_9
Lake.Build.Facets
Batteries.Data.List.Count
Aesop.RuleTac.Forward
Acmoi.Exercise4_1
Qq.ForLean.ToExpr
Batteries.Lean.MonadBacktrack
Aesop.BuiltinRules.Intros
Aesop.RuleTac.FVarIdSubst
Batteries.Data.Rat.Basic
Lake.Build.Job
Batteries.Tactic.PermuteGoals
Batteries.Lean.Float
Batteries.CodeAction.Basic
Qq.SortLocalDecls
Batteries.Tactic.Unreachable
Aesop.Index.Basic
Aesop.Search.RuleSelection
Lake.DSL.Script
Acmoi.Exercise2_567
Batteries.Util.LibraryNote
Lake.Util.Binder
ProofWidgets.Component.OfRpcMethod
Lake.Config.Package
Batteries.Data.Nat.Gcd
Lake.Config.Defaults
Acmoi.dimVC
Batteries.Lean.Meta.DiscrTree
LeanSearchClient.Basic
Aesop.Tree.State
Aesop.Tree.RunMetaM
Aesop.BuiltinRules.Subst
Lake.DSL.Meta
Aesop.Script.Step
Aesop.Script.SpecificTactics
Lake.DSL.Require
Acmoi.Basic
Lake.Toml.ParserUtil
Batteries.Tactic.Lint.Basic
Aesop.Tracing
Batteries.Data.String.Basic
Batteries.Lean.NameMap
Aesop.Script.GoalWithMVars
Batteries.Tactic.Lint.Simp
ProofWidgets.Component.Panel.Basic
Batteries.Linter.UnnecessarySeqFocus
Aesop.Frontend.Tactic
Batteries.Data.BinomialHeap.Basic
Qq.Macro
Lake.DSL.Config
Aesop.Tree.Data
Lake.Build.Store
Lake.DSL.Targets
Aesop.Search.Expansion.Norm
Aesop.Util.Tactic.Ext
Lake.Build.Targets
Acmoi.Exercise1_19
Lake.Load.Config
Batteries.Tactic.Where
Aesop.Frontend.Extension.Init
Aesop.RulePattern
Aesop.Script.StructureStatic
Lake.Build.Fetch
Aesop.BuiltinRules.ApplyHyps
Aesop.Search.Expansion.Simp
Batteries.Util.Cache
Aesop.Builder.Cases
Lake.Util.Task
ProofWidgets.Component.PenroseDiagram
Batteries.Tactic.Init
Batteries.Classes.RatCast
Batteries.Data.Array.Init.Lemmas
Lake.Config.Opaque
Acmoi.Exercise7_1
Aesop.ElabM
Acmoi.Exercise6_1
Batteries.Data.Rat.Lemmas
Lake.Util.List
Batteries.Lean.PersistentHashMap
Aesop.Builder.Apply
Lake.Build.Library
ProofWidgets.Data.Html
Acmoi.HydePrelim
Acmoi.Exercise1_7
Aesop.RuleSet.Name
Lake.Util.Cycle
Acmoi
Aesop.Search.Expansion.Basic
Aesop.Tree.TreeM
Aesop.RuleTac.GoalDiff
Aesop.RuleTac.Preprocess
Lake.Util.Proc
Aesop.Saturate
Aesop.Builder.Constructors
Lake.Build.Info
Lake.CLI.Build
Acmoi.Exercise7_2
Batteries.Util.ExtendedBinder
Aesop.Check
Lake.Config.LeanExeConfig
Aesop.RuleSet
Lake.Build.Run
Batteries.CodeAction.Deprecated