Documentation
Lean
.
Meta
Search
Google site search
return to top
source
Imports
Init
Lean.Meta.AbstractMVars
Lean.Meta.AbstractNestedProofs
Lean.Meta.AppBuilder
Lean.Meta.Basic
Lean.Meta.CasesOn
Lean.Meta.Closure
Lean.Meta.Coe
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.KAbstract
Lean.Meta.LevelDefEq
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