Documentation

Lean.Elab.Tactic.RCases

Enables the 'unused rcases pattern' linter. This will warn when a pattern is ignored by rcases, rintro, ext and similar tactics.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean :
Coe (Lean.TSyntax `Lean.Parser.Tactic.rcasesPatMed) (Lean.TSyntax `Lean.Parser.Tactic.rcasesPatLo)
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

An rcases pattern can be one of the following, in a nested combination:

  • A name like foo
  • The special keyword rfl (for pattern matching on equality using subst)
  • A hyphen -, which clears the active hypothesis and any dependents.
  • A type ascription like pat : ty (parentheses are optional)
  • A tuple constructor like ⟨p1, p2, p3⟩
  • An alternation / variant pattern p1 | p2 | p3

Parentheses can be used for grouping; alternation is higher precedence than type ascription, so p1 | p2 | p3 : ty means (p1 | p2 | p3) : ty.

N-ary alternations are treated as a group, so p1 | p2 | p3 is not the same as p1 | (p2 | p3), and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary conjunction or disjunction, because if the number of patterns exceeds the number of constructors in the type being destructed, the extra patterns will match on the last element, meaning that p1 | p2 | p3 will act like p1 | (p2 | p3) when matching a1 ∨ a2 ∨ a3. If matching against a type with 3 constructors, p1 | (p2 | p3) will act like p1 | (p2 | p3) | _ instead.

Instances For

    Interpret an rcases pattern as a tuple, where p becomes ⟨p⟩ if p is not already a tuple.

    Equations
    Instances For

      Interpret an rcases pattern as an alternation, where non-alternations are treated as one alternative.

      Equations
      Instances For

        Convert a list of patterns to an alternation pattern, but mapping [p] to p instead of a unary alternation |p.

        Equations
        Instances For

          This function is used for producing rcases patterns based on a case tree. Suppose that we have a list of patterns ps that will match correctly against the branches of the case tree for one constructor. This function will merge tuples at the end of the list, so that [a, b, ⟨c, d⟩] becomes ⟨a, b, c, d⟩ instead of ⟨a, b, ⟨c, d⟩⟩.

          We must be careful to turn [a, ⟨⟩] into ⟨a, ⟨⟩⟩ instead of ⟨a⟩ (which will not perform the nested match).

          Equations
          Instances For

            This function is used for producing rcases patterns based on a case tree. This is like tuple₁Core but it produces a pattern instead of a tuple pattern list, converting [n] to n instead of ⟨n⟩ and [] to _, and otherwise just converting [a, b, c] to ⟨a, b, c⟩.

            Equations
            Instances For

              This function is used for producing rcases patterns based on a case tree. Here we are given the list of patterns to apply to each argument of each constructor after the main case, and must produce a list of alternatives with the same effect. This function calls tuple₁ to make the individual alternatives, and handles merging [a, b, c | d] to a | b | c | d instead of a | b | (c | d).

              Equations
              Instances For

                This function is used for producing rcases patterns based on a case tree. This is like alts₁Core, but it produces a cases pattern directly instead of a list of alternatives. We specially translate the empty alternation to ⟨⟩, and translate |(a | b) to ⟨a | b⟩ (because we don't have any syntax for unary alternation). Otherwise we can use the regular merging of alternations at the last argument so that a | b | (c | d) becomes a | b | c | d.

                Equations
                Instances For

                  parenthesize the message if the precedence is above tgt

                  Equations
                  Instances For

                    format an RCasesPatt with the given precedence: 0 = lo, 1 = med, 2 = hi

                    @[irreducible]

                    Takes the number of fields of a single constructor and patterns to match its fields against (not necessarily the same number). The returned lists each contain one element per field of the constructor. The name is the name which will be used in the top-level cases tactic, and the rcases_patt is the pattern which the field will be matched against by subsequent cases tactics.

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

                      Takes a list of constructor names, and an (alternation) list of patterns, and matches each pattern against its constructor. It returns the list of names that will be passed to cases, and the list of (constructor name, patterns) for each constructor, where patterns is the (conjunctive) list of patterns to apply to each constructor argument.

                      Equations
                      Instances For

                        Like Lean.Meta.subst, but preserves the FVarSubst.

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

                          This will match a pattern pat against a local hypothesis e.

                          • g: The initial subgoal
                          • fs: A running variable substitution, the result of cases operations upstream. The variable e must be run through this map before locating it in the context of g, and the output variable substitutions will be end extensions of this one.
                          • clears: The list of variables to clear in all subgoals generated from this point on. We defer clear operations because clearing too early can cause cases to fail. The actual clearing happens in RCases.finish.
                          • e: a local hypothesis, the scrutinee to match against.
                          • a: opaque "user data" which is passed through all the goal calls at the end.
                          • pat: the pattern to match against
                          • cont: A continuation. This is called on every goal generated by the result of the pattern match, with updated values for g , fs, clears, and a.

                          Runs rcasesContinue on the first pattern in r with a matching ctorName. The unprocessed patterns (subsequent to the matching pattern) are returned.

                          This will match a list of patterns against a list of hypotheses e. The arguments are similar to rcasesCore, but the patterns and local variables are in pats. Because the calls are all nested in continuations, later arguments can be matched many times, once per goal produced by earlier arguments. For example ⟨a | b, ⟨c, d⟩⟩ performs the ⟨c, d⟩ match twice, once on the a branch and once on b.

                          Like tryClearMany, but also clears dependent hypotheses if possible

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

                            The terminating continuation used in rcasesCore and rcasesContinue. We specialize the type α to Array MVarId to collect the list of goals, and given the list of clears, it attempts to clear them from the goal and adds the goal to the list.

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

                              Parses a Syntax into the RCasesPatt type used by the RCases tactic.

                              Generalize all the arguments as specified in args to fvars if they aren't already

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

                                Given a list of targets of the form e or h : e, and a pattern, match all the targets against the pattern. Returns the list of produced subgoals.

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

                                  The obtain tactic in the no-target case. Given a type T, create a goal |- T and and pattern match T against the given pattern. Returns the list of goals, with the assumed goal first followed by the goals produced by the pattern match.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    partial def Lean.Elab.Tactic.RCases.expandRIntroPat (pat : Lean.TSyntax `rintroPat) (acc : optParam (Array (Lean.TSyntax `rcasesPat)) #[]) (ty? : optParam (Option Lean.Term) none) :
                                    Array (Lean.TSyntax `rcasesPat)

                                    Expand a rintroPat into an equivalent list of rcasesPat patterns.

                                    partial def Lean.Elab.Tactic.RCases.expandRIntroPats (pats : Array (Lean.TSyntax `rintroPat)) (acc : optParam (Array (Lean.TSyntax `rcasesPat)) #[]) (ty? : optParam (Option Lean.Term) none) :
                                    Array (Lean.TSyntax `rcasesPat)

                                    Expand a list of rintroPat into an equivalent list of rcasesPat patterns.

                                    This introduces the pattern pat. It has the same arguments as rcasesCore, plus:

                                    • ty?: the nearest enclosing type ascription on the current pattern

                                    This introduces the list of patterns pats. It has the same arguments as rcasesCore, plus:

                                    • ty?: the nearest enclosing type ascription on the current pattern

                                    Runs rintroContinue on pats[i:]

                                    The implementation of the rintro tactic. It takes a list of patterns pats and an optional type ascription ty? and introduces the patterns, resulting in zero or more goals.

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