Documentation
Lean
.
Elab
.
Tactic
.
Grind
.
Anchor
Search
return to top
source
Imports
Lean.Meta.Tactic.Grind.Types
Imported by
Lean
.
Elab
.
Tactic
.
Grind
.
elabAnchorRef
source
def
Lean
.
Elab
.
Tactic
.
Grind
.
elabAnchorRef
(
anchor
:
TSyntax
`hexnum
)
:
CoreM
Meta.Grind.AnchorRef
Equations
One or more equations did not get rendered due to their size.
Instances For