def Std.Tactic.NthConstructor.nthConstructor (name : Lean.Name) (idx : Nat) (max : Option Nat) (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Apply the n-th constructor of the target type, checking that it is an inductive type, and that there are the expected number of constructors.

Equations

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

def Std.Tactic.tacticLeft : Lean.ParserDescr

Apply the first constructor, in the case that the goal is an inductive type with exactly two constructors.

example : True ∨ False := by
  left
  trivial

Equations

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

def Std.Tactic.tacticRight : Lean.ParserDescr

Apply the second constructor, in the case that the goal is an inductive type with exactly two constructors.

example {p q : Prop} (h : q) : p ∨ q := by
  right
  exact h

Equations

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