Documentation
Lean
.
Elab
.
PreDefinition
.
Nonrec
.
Eqns
Search
return to top
source
Imports
Init.Data.Array.Basic
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.Eqns
Lean.Meta.ArgsPacker.Basic
Lean.Meta.Tactic.Rewrite
Lean.Meta.Tactic.Split
Imported by
Lean
.
Elab
.
Nonrec
.
getEqnsFor?
source
def
Lean
.
Elab
.
Nonrec
.
getEqnsFor?
(
declName
:
Name
)
:
MetaM
(
Option
(
Array
Name
)
)
Equations
Instances For