def Lean.Parser.Tactic.unknown : Parser

Equations

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

def Lean.Parser.Tactic.nestedTactic : Parser

Equations

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

def Lean.Parser.Tactic.matchRhs : Parser

Equations

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

def Lean.Parser.Tactic.matchAlts : Parser

Equations

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

def Lean.Parser.Tactic.match : 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 : Parser

Introduces one or more hypotheses, optionally naming and/or pattern-matching them. For each hypothesis to be introduced, the remaining main goal's target type must be a let or function type.

• intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption. It is equivalent to intro _.
• intro x y introduces two hypotheses and names them. Individual hypotheses can be anonymized via _, given a type ascription, or matched against a pattern:

  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  

• intro rfl is short for intro h; subst h, if h is an equality where the left-hand or right-hand side is a variable.
• Alternatively, intro can be combined with pattern matching much like fun:

  intro
  | n + 1, 0 => tac
  | ...
  

Equations

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