def DY.Step.stepIntro (mvar : Lean.MVarId) : Lean.Elab.Tactic.TacticM (Lean.FVarId × Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.

def DY.Step.step_intro : Lean.ParserDescr

Equations

• DY.Step.step_intro = Lean.ParserDescr.node `DY.Step.step_intro 1024 (Lean.ParserDescr.nonReservedSymbol "step_intro" false)

def DY.Step.tacticHoist : Lean.ParserDescr

Equations

• DY.Step.tacticHoist = Lean.ParserDescr.node `DY.Step.tacticHoist 1024 (Lean.ParserDescr.nonReservedSymbol "hoist" false)