Documentation
Lean
.
Elab
.
PreDefinition
.
PartialFixpoint
.
Induction
Search
return to top
source
Imports
Lean.Meta.ArgsPacker
Lean.Meta.Injective
Init.Internal.Order.Basic
Lean.Meta.Tactic.ElimInfo
Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Meta.Match.MatcherApp.Transform
Imported by