• pi : list name → ℕ → tactic.interactive.case_tag
• hyps : list name → list name → tactic.interactive.case_tag

A case tag carries the following information:

1. A list of names identifying the case ('case names'). This is usually a list of constructor names, one for each case split that was performed. For example, the sequence of tactics cases n; cases xs, where n is a natural number and xs is a list, will generate four cases tagged as follows:

   nat.zero, list.nil
   nat.zero, list.cons
   nat.succ, list.nil
   nat.succ, list.cons
   

   Note: In the case tag, the case names are stored in reverse order. Thus, the case names of the first case tag would be list.nil, nat.zero. This is because when printing a goal tag (as part of a goal state), Lean prints all non-internal names in reverse order.

2. Information about the arguments introduced by the cases-like tactic. Different tactics work slightly different in this regard:

   1. The with_cases tactic generates goals where the target quantifies over any added hypotheses. For example, with_cases { cases xs }, where xs is a list α, will generate a target of the form α → list α → ... in the cons case, where the two arguments correspond to the two arguments of the cons constructor. Goals of this form are tagged with a pi case tag (since the target is a pi type). In addition to the case names, it contains a natural number, num_arguments, which specifies how many of the arguments that the target quantifies over were introduced by with_cases.

      For example, given n : ℕ and xs : list α, the fourth goal generated by with_cases { cases n; induction xs } has this form:

      ...
      ⊢ ℕ → α → ∀ (xs' : list α), P xs' → ...
      

      The corresponding case tag is

      pi [`list.cons, `nat.succ] 4
      

      since the first four arguments of the target were introduced by with_cases {...}.

   2. The cases and induction tactics do not add arguments to the target, but rather introduce them as hypotheses in the local context. Goals of this form are tagged with a hyps case tag. In addition to the case names, it contains a list of unique names of the hypotheses that were introduced.

      For example, given xs : list α, the second goal generated by induction xs has this form:

      ...
      x : α
      xs' : list α
      ih_xs' : P xs'
      ⊢ ...
      

      The corresponding goal tag is

      hyps [`list.cons] [`<x>, `<xs'>, `<ih_xs'>]
      

      where `<h> denotes the unique name of a hypothesis h.

      Note: Many tactics do not preserve the unique names of hypotheses (particularly those tactics that use revert). Therefore, a hyps case tag is only guaranteed to be valid directly after it was generated.

• exact_match : tactic.interactive.case_tag.match_result
• fuzzy_match : tactic.interactive.case_tag.match_result
• no_match : tactic.interactive.case_tag.match_result

Indicates the result of matching a list of names against the names of a case tag. See match_tag.