Documentation

Init

return to top

source

Imports

Init.BinderNameHint
Init.BinderPredicates
Init.ByCases
Init.Control
Init.Conv
Init.Core
Init.Data
Init.Dynamic
Init.Ext
Init.Grind
Init.Guard
Init.Hints
Init.Internal
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.Syntax
Init.System
Init.Tactics
Init.TacticsExtra
Init.Task
Init.Try
Init.Util
Init.WF
Init.WFTactics
Init.While
Init.Data.Basic

Imported by

KoszulComplex.DGA
Aesop.Rule.Name
Batteries.Lean.TagAttribute
Aesop.BuiltinRules.ApplyHyps
Batteries.Data.HashMap.Basic
Aesop.Index.DiscrTreeConfig
Aesop.ElabM
Aesop.BaseM
Batteries.Lean.HashSet
Aesop.Script.GoalWithMVars
Aesop.Tree.TreeM
Batteries.Data.BinomialHeap.Lemmas
Aesop.Search.Main
LeanSearchClient.Syntax
ProofWidgets.Presentation.Expr
Aesop.Search.Queue
LeanSearchClient.Basic
Batteries.Data.Vector.Basic
Aesop.Options.Public
Batteries.Lean.Meta.UnusedNames
Aesop.Tree
Batteries.Control.Lawful.MonadLift
Batteries.Data.List.Count
Batteries.Data.AssocList
Batteries.Tactic.Lint.Basic
Aesop.RPINF
Batteries.Util.Cache
Batteries.Data.String.Basic
Aesop.Script.Tactic
Batteries.Data.Fin.OfBits
Batteries.Control.AlternativeMonad
Aesop.Tree.State
Batteries.Data.Rat.Basic
Batteries.Data.List.ArrayMap
Batteries.Data.RBMap
Aesop.Tree.Traversal
Aesop.RuleTac.Apply
Aesop.Script.ScriptM
Aesop.Frontend.Extension.Init
Batteries.Data.UnionFind.Lemmas
Aesop.Frontend.Command
Aesop.BuiltinRules.Subst
Aesop.Tree.ExtractScript
Aesop.Util.Tactic.Unfold
Aesop.Constants
Aesop.Frontend.RuleExpr
Batteries.Data.Range
Batteries.Classes.RatCast
Aesop.RPINF.Basic
Batteries.Data.Array.Match
Batteries.Data.MLList.Heartbeats
ProofWidgets.Component.PenroseDiagram
Batteries.Tactic.Exact
Aesop.Builder.Basic
Batteries.Data.Range.Lemmas
Aesop.Rule.Basic
Batteries.Tactic.Alias
Batteries.Data.List.Pairwise
Batteries.Data.UnionFind.Basic
Batteries.Lean.SatisfiesM
Aesop.Main
Aesop.Nanos
Qq.ForLean.Do
Batteries.Tactic.Unreachable
Batteries.Data.List
Batteries.Tactic.Lint
Aesop.BuiltinRules
ProofWidgets.Component.OfRpcMethod
Aesop.Script.OptimizeSyntax
Batteries.Data.List.Lemmas
Batteries.Data.HashMap
Aesop.Rule
Aesop.RuleTac.Forward.Basic
Batteries.Tactic.Instances
Aesop.Script.Check
Batteries.Data.BitVec
Qq.SortLocalDecls
Aesop.RuleSet.Member
Batteries.Data.MLList.IO
Batteries.Data.Random
ProofWidgets.Component.Basic
Aesop.Search.Expansion.Simp
Aesop.Script.StructureDynamic
Batteries.Data.Stream
Aesop.Util.Tactic
Aesop.Rule.Forward
Aesop.Stats.Basic
Aesop.Util.Tactic.Ext
Aesop.Search.Queue.Class
Aesop.Index.RulePattern
Batteries.Lean.Float
Aesop.Tree.Tracing
Aesop.RuleTac.Tactic
Aesop.Percent
Batteries.Lean.IO.Process
Plausible.Random
Batteries.Data.Int
Batteries.Data.Rat.Float
Batteries.Data.Nat
Batteries.Data.Array.Lemmas
Batteries.Lean.Meta.Basic
Batteries.Data.Nat.Gcd
Aesop.RuleTac
ProofWidgets.Compat
Batteries.Lean.Position
KoszulComplex.Defs
Aesop.Check
Batteries.Data.RBMap.Basic
Plausible.Testable
Batteries.Data.ByteArray
Batteries.Data.Char
Batteries.Lean.System.IO
Aesop.Search.ExpandSafePrefix
Aesop.BuiltinRules.Split
Batteries.Lean.Json
Aesop.Search.Expansion
Aesop.RuleTac.Forward
ImportGraph.RequiredModules
Batteries.Data.String
Batteries.Data.RBMap.Lemmas
Batteries.Data.Fin.Lemmas
Aesop.Index
Batteries.Lean.AttributeExtra
Batteries.Linter.UnreachableTactic
Aesop.RuleTac.Descr
Aesop.Script.UScript
ProofWidgets.Data.Html
Aesop.RuleTac.FVarIdSubst
Batteries.Tactic.Lint.TypeClass
Aesop.Script.Step
Batteries.Data.ByteSubarray
Batteries.Tactic.Congr
Aesop.Forward.State
LeanSearchClient.LoogleSyntax
Aesop.Tree.RunMetaM
Aesop.Saturate
Batteries.Data.RBMap.Depth
Batteries.CodeAction.Attr
Batteries.Tactic.Lint.Frontend
Aesop.Search.SearchM
KoszulComplex.cycleIcc
Aesop.Frontend.Basic
Qq.MetaM
Batteries.Tactic.PrintDependents
Lean
Aesop.Forward.RuleInfo
Batteries.Linter
Batteries.Data.List.Perm
Batteries.CodeAction.Deprecated
Batteries.Data.Vector.Lemmas
Batteries.Tactic.Trans
Batteries.Lean.Util.EnvSearch
Aesop.Builder.Constructors
Batteries.Data.BinomialHeap.Basic
Aesop.Util.UnionFind
Batteries.Data.BitVec.Basic
ProofWidgets.Cancellable
Batteries.Data.BinaryHeap
Batteries.Lean.Syntax
Batteries.Util.Pickle
Batteries.Data.Array.Monadic
Aesop.Options.Internal
Batteries.Tactic.SeqFocus
Qq.Typ
Batteries.CodeAction
Aesop.Script.TacticState
Aesop.Tree.AddRapp
Batteries.Tactic.PrintPrefix
Aesop.Forward.Match.Types
Aesop.Builder.Default
Batteries.Tactic.PermuteGoals
Batteries.Classes.Order
Batteries.Data.UInt
Batteries.Data.DList
Aesop.Forward.State.ApplyGoalDiff
Batteries.Data.Random.MersenneTwister
Aesop.Search.Expansion.Basic
Batteries.Data.Rat.Lemmas
Batteries.Control.OptionT
Batteries.Tactic.Case
Batteries.Linter.UnnecessarySeqFocus
Aesop.Stats.Report
Batteries.Data.UnionFind
Batteries.Tactic.ShowUnused
Batteries.Tactic.Init
Aesop.Search.Expansion.Norm
Aesop.Forward.State.Initial
Batteries.Data.Nat.Lemmas
Aesop.BuiltinRules.Intros
Batteries.Data.Fin.Fold
Aesop.Util.EqualUpToIds
Batteries.Data.HashMap.Lemmas
Batteries.CodeAction.Basic
Aesop.RuleTac.GoalDiff
Aesop.Tracing
Aesop.Options
Aesop.Util.Basic
Batteries.Data.RBMap.Alter
Aesop.Script.SpecificTactics
Batteries.Data.DList.Lemmas
Batteries.Data.List.Matcher
Batteries.Tactic.PrintOpaques
Batteries.Data.Vector.Monadic
Batteries.Classes.SatisfiesM
Batteries.Data.Fin.Basic
Aesop.Builder.Tactic
Batteries.Data.Vector
Plausible.Gen
Aesop.Frontend.Extension
Batteries.Data.Array.OfFn
Batteries.Lean.Expr
Batteries.Data.BinomialHeap
Batteries.Control.ForInStep.Basic
Batteries.Lean.LawfulMonadLift
Batteries.Control.ForInStep
Batteries.Data.String.Matcher
Batteries.Util.Panic
Batteries.Lean.LawfulMonad
Batteries.Data.Rat
Aesop.Forward.Match
Batteries.Tactic.Basic
Batteries.Data.String.Lemmas
Batteries.Lean.Meta.InstantiateMVars
Batteries.Util.ExtendedBinder
Batteries.Lean.Meta.SavedState
ImportGraph.Imports
Aesop.RuleSet.Filter
Batteries.Lean.PersistentHashMap
Aesop.Forward.PremiseIndex
Batteries.Util.ProofWanted
Qq.ForLean.ReduceEval
Aesop.BuiltinRules.Assumption
Batteries.Data.List.Basic
Aesop.RuleSet
Batteries.Data.Array
Aesop.RuleTac.RuleTerm
Batteries.Tactic.NoMatch
Batteries.Util.LibraryNote
Aesop.Script.CtorNames
Batteries.Control.Lemmas
Aesop.Frontend.Tactic
Aesop.Tree.Free
Plausible.Attr
Batteries.Logic
Batteries.Lean.MonadBacktrack
ProofWidgets.Util
Aesop.RulePattern
Batteries.Data.Nat.Basic
Batteries.Lean.NameMapAttribute
Aesop.Script.UScriptToSScript
Qq.Simp
Batteries.Lean.Meta.Expr
Qq.ForLean.ToExpr
Batteries.Tactic.HelpCmd
Batteries.Data.Array.Init.Lemmas
Batteries.Lean.EStateM
Batteries.Control.Nondet.Basic
Aesop.Script.Main
Aesop.Tree.Data.ForwardRuleMatches
Aesop.Builder.NormSimp
Batteries.Tactic.SqueezeScope
Batteries.Lean.PersistentHashSet
Batteries.Data.Array.Basic
Qq.Macro
Aesop.BuiltinRules.Ext
Batteries.Lean.Meta.Inaccessible
Batteries.Data.Array.Merge
Aesop.Forward.SlotIndex
Aesop.RulePattern.Cache
ProofWidgets.Component.MakeEditLink
Batteries.Data.Fin
Batteries.Data.BitVec.Lemmas
Aesop.Script.Util
Batteries.Data.List.Init.Lemmas
Batteries.Control.Monad
Aesop.Builder.Forward
Aesop.BuiltinRules.DestructProducts
Batteries.Tactic.OpenPrivate
Batteries.Lean.HashMap
Aesop.Forward.LevelIndex
Aesop.Builder.Apply
Aesop.Index.Basic
Batteries.Data.NameSet
Qq.AssertInstancesCommute
Plausible.Functions
Aesop.RuleSet.Name
ProofWidgets.Component.Panel.Basic
Aesop.Util.UnorderedArraySet
Aesop.Builder.Cases
Batteries.Lean.Except
Aesop.Tree.Data
Aesop.Tree.UnsafeQueue
Aesop.RuleTac.ElabRuleTerm
Batteries.Data.Nat.Bisect
Qq.Match
Qq.Delab
Batteries.CodeAction.Misc
Batteries.Data.PairingHeap
Batteries.Data.FloatArray
Batteries.WF
Plausible.Sampleable
Aesop.Tree.ExtractProof
Batteries.Data.DList.Basic
Batteries.Classes.Cast
Batteries.Lean.Meta.Simp
Aesop.BuiltinRules.Rfl
ProofWidgets.Component.HtmlDisplay
Batteries.Data.List.Monadic
Batteries.Tactic.Lint.Misc
Aesop.Stats.Extension
Batteries.Lean.Meta.DiscrTree
Aesop.RuleTac.Preprocess
Batteries.Data.MLList.Basic
Batteries.Control.ForInStep.Lemmas
Aesop.Exception
Batteries.Data.List.OfFn
Batteries.Data.RBMap.WF
Aesop.Index.Forward
Aesop.Builder.Unfold
Aesop.Forward.Substitution
Plausible.Tactic
Batteries.Tactic.Lemma
Aesop.Frontend.Saturate
Aesop.RuleTac.Basic
KoszulComplex
Aesop.Frontend.Attribute
Batteries.Data.MLList
Aesop.RuleTac.Cases
Aesop.Tree.Check
Aesop.Search.RuleSelection
Batteries.Data.Array.Pairwise
Aesop.Script.StructureStatic
Aesop.Script.SScript
Batteries.Tactic.Lint.Simp