opaque Lean.Elab.Tactic.RCases.linter.unusedRCasesPattern : Lean.Option Bool

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

instance Lean.Elab.Tactic.RCases.instCoeIdentTSyntaxConsSyntaxNodeKindMkStr1Nil_lean : Coe Ident (TSyntax `rcasesPat)

Equations

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

instance Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1NilMkStr4_lean : Coe (TSyntax `rcasesPat) (TSyntax `Lean.Parser.Tactic.rcasesPatMed)

Equations

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

instance Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean : Coe (TSyntax `Lean.Parser.Tactic.rcasesPatMed) (TSyntax `Lean.Parser.Tactic.rcasesPatLo)

Equations

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

instance Lean.Elab.Tactic.RCases.instCoeTSyntaxConsSyntaxNodeKindMkStr1Nil_lean : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat)

Equations

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

inductive Lean.Elab.Tactic.RCases.RCasesPatt : Type

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.

• paren (ref : Syntax) : RCasesPatt → RCasesPatt

  A parenthesized expression, used for hovers

• one (ref : Syntax) : Name → RCasesPatt

  A named pattern like foo

• clear (ref : Syntax) : RCasesPatt

  A hyphen -, which clears the active hypothesis and any dependents.

• explicit (ref : Syntax) : RCasesPatt → RCasesPatt

  An explicit pattern @pat.

• typed (ref : Syntax) : RCasesPatt → Term → RCasesPatt

  A type ascription like pat : ty (parentheses are optional)

• tuple (ref : Syntax) : List RCasesPatt → RCasesPatt

  A tuple constructor like ⟨p1, p2, p3⟩

• alts (ref : Syntax) : List RCasesPatt → RCasesPatt

  An alternation / variant pattern p1 | p2 | p3

instance Lean.Elab.Tactic.RCases.instReprRCasesPatt : Repr RCasesPatt

Equations

• Lean.Elab.Tactic.RCases.instReprRCasesPatt = { reprPrec := Lean.Elab.Tactic.RCases.instReprRCasesPatt.repr }

partial def Lean.Elab.Tactic.RCases.instReprRCasesPatt.repr : RCasesPatt → Nat → Format

def Lean.Elab.Tactic.RCases.rcases (tgts : Array (Option Ident × Syntax)) (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId)

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.

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

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

def Lean.Elab.Tactic.RCases.rintro (pats : TSyntaxArray `rintroPat) (ty? : Option Term) (g : MVarId) : TermElabM (List MVarId)

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.