def Mathlib.Tactic.LeftRight.leftRightMeta (name : Lean.Name) (idx : Nat) (max : Nat) (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Equations

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

def Mathlib.Tactic.tacticLeft : Lean.ParserDescr

Equations

• Mathlib.Tactic.tacticLeft = Lean.ParserDescr.node `Mathlib.Tactic.tacticLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)

def Mathlib.Tactic.tacticRight : Lean.ParserDescr

Equations

• Mathlib.Tactic.tacticRight = Lean.ParserDescr.node `Mathlib.Tactic.tacticRight 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)