Documentation
Lean
.
Meta
Search
return to top
source
Imports
Lean.Meta.AbstractMVars
Lean.Meta.AbstractNestedProofs
Lean.Meta.AppBuilder
Lean.Meta.Basic
Lean.Meta.BinderNameHint
Lean.Meta.Canonicalizer
Lean.Meta.CheckTactic
Lean.Meta.Closure
Lean.Meta.Coe
Lean.Meta.CoeAttr
Lean.Meta.CollectFVars
Lean.Meta.CongrTheorems
Lean.Meta.Constructions
Lean.Meta.CtorIdxHInj
Lean.Meta.DecLevel
Lean.Meta.Diagnostics
Lean.Meta.DiscrTree
Lean.Meta.Eqns
Lean.Meta.Eval
Lean.Meta.ExprDefEq
Lean.Meta.ExprLens
Lean.Meta.ExprTraverse
Lean.Meta.ForEachExpr
Lean.Meta.FunInfo
Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeVars
Lean.Meta.HasAssignableMVar
Lean.Meta.HaveTelescope
Lean.Meta.Hint
Lean.Meta.IndPredBelow
Lean.Meta.Inductive
Lean.Meta.InferType
Lean.Meta.Injective
Lean.Meta.Instances
Lean.Meta.Iterator
Lean.Meta.KAbstract
Lean.Meta.LazyDiscrTree
Lean.Meta.LetToHave
Lean.Meta.LevelDefEq
Lean.Meta.LitValues
Lean.Meta.Match
Lean.Meta.MethodSpecs
Lean.Meta.MonadSimp
Lean.Meta.PPGoal
Lean.Meta.RecursorInfo
Lean.Meta.Reduce
Lean.Meta.ReduceEval
Lean.Meta.SizeOf
Lean.Meta.Sorry
Lean.Meta.Structure
Lean.Meta.Sym
Lean.Meta.SynthInstance
Lean.Meta.Tactic
Lean.Meta.Transform
Lean.Meta.TryThis
Lean.Meta.UnificationHint
Lean.Meta.WHNF
Lean.Meta.WrapInstance
Imported by
← Mathematical handbook