Documentation
Lean
.
Meta
Search
Google site search
return to top
source
Imports
Lean.Meta.AbstractMVars
Lean.Meta.AbstractNestedProofs
Lean.Meta.AppBuilder
Lean.Meta.Basic
Lean.Meta.Closure
Lean.Meta.Coe
Lean.Meta.CoeAttr
Lean.Meta.CollectFVars
Lean.Meta.CongrTheorems
Lean.Meta.Constructions
Lean.Meta.DecLevel
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.IndPredBelow
Lean.Meta.Inductive
Lean.Meta.InferType
Lean.Meta.Injective
Lean.Meta.Instances
Lean.Meta.Iterator
Lean.Meta.KAbstract
Lean.Meta.LazyDiscrTree
Lean.Meta.LevelDefEq
Lean.Meta.LitValues
Lean.Meta.Match
Lean.Meta.PPGoal
Lean.Meta.RecursorInfo
Lean.Meta.Reduce
Lean.Meta.ReduceEval
Lean.Meta.SizeOf
Lean.Meta.Structure
Lean.Meta.SynthInstance
Lean.Meta.Tactic
Lean.Meta.Transform
Lean.Meta.UnificationHint
Lean.Meta.WHNF
Imported by