def Lean.Parser.Tactic.unknown : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.nestedTactic : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.nestedTactic = Lean.Parser.Tactic.tacticSeqBracketed

def Lean.Parser.Tactic.matchRhs : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchRhs = (Lean.Parser.Term.hole <|> Lean.Parser.Term.syntheticHole <|> Lean.Parser.Tactic.tacticSeq)

def Lean.Parser.Tactic.matchAlts : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.matchAlts = Lean.Parser.Term.matchAlts Lean.Parser.Tactic.matchRhs

def Lean.Parser.Tactic.match : Lean.Parser.Parser

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | i+1 => simp

Equations

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

def Lean.Parser.Tactic.introMatch : Lean.Parser.Parser

The tactic

intro
| pat1 => tac1
| pat2 => tac2

is the same as:

intro x
match x with
| pat1 => tac1
| pat2 => tac2

That is, intro can be followed by match arms and it introduces the values while doing a pattern match. This is equivalent to fun with match arms in term mode.

Equations

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