Documentation

Lean.Parser.Tactic

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For

              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
                Instances For

                  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
                    Instances For