Fixes

This PR lets `induction` print a warning if a variable occurring in the
`using` clause is generalized. Fixes #10683.

src/Lean/Elab/Tactic/Ext.lean

@@ -6,16 +6,13 @@ Authors: Gabriel Ebner, Mario Carneiro
 module
 
 prelude
-public import Init.Ext
-public import Lean.Meta.Tactic.Ext
-public import Lean.Elab.DeclarationRange
-public import Lean.Elab.Tactic.RCases
-public import Lean.Elab.Tactic.Repeat
-public import Lean.Elab.Tactic.BuiltinTactic
-public import Lean.Elab.Command
-public import Lean.Linter.Basic
-
-public section
+import Lean.Meta.Tactic.Ext
+import Lean.Elab.DeclarationRange
+import Lean.Elab.Tactic.RCases
+import Lean.Elab.Tactic.Repeat
+import Lean.Elab.Tactic.BuiltinTactic
+import Lean.Elab.Command
+import Lean.Linter.Basic
 
 /-!
 # Implementation of the `@[ext]` attribute

src/Lean/Elab/Tactic/Induction.lean

@@ -6,23 +6,22 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Lean.Util.CollectFVars
-public import Lean.AuxRecursor
-public import Lean.Parser.Term
-public import Lean.Meta.RecursorInfo
-public import Lean.Meta.CollectMVars
+public import Lean.Meta.Basic
 public import Lean.Meta.Tactic.ElimInfo
-public import Lean.Meta.Tactic.FunIndInfo
-public import Lean.Meta.Tactic.Induction
-public import Lean.Meta.Tactic.Cases
-public import Lean.Meta.Tactic.FunIndCollect
-public import Lean.Meta.GeneralizeVars
-public import Lean.Elab.App
-public import Lean.Elab.Match
 public import Lean.Elab.Tactic.ElabTerm
-public import Lean.Elab.Tactic.Generalize
-
-public section
+import Lean.Util.CollectFVars
+import Lean.AuxRecursor
+import Lean.Parser.Term
+import Lean.Meta.RecursorInfo
+import Lean.Meta.CollectMVars
+import Lean.Meta.Tactic.FunIndInfo
+import Lean.Meta.Tactic.Induction
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.FunIndCollect
+import Lean.Meta.GeneralizeVars
+import Lean.Elab.App
+import Lean.Elab.Match
+import Lean.Elab.Tactic.Generalize
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -36,12 +35,12 @@ open Meta
   We assume that the syntax has been expanded. There is exactly one `inductionAltLHS`,
   and `" => " (hole <|> syntheticHole <|> tacticSeq)` is present
 -/
-private def getAltLhses (alt : Syntax) : Syntax :=
+def getAltLhses (alt : Syntax) : Syntax :=
   alt[0]
-private def getFirstAltLhs (alt : Syntax) : Syntax :=
+def getFirstAltLhs (alt : Syntax) : Syntax :=
   (getAltLhses alt)[0]
 /-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS`. Returns `none` if the name is missing. -/
-private def getAltName? (alt : Syntax) : Option Name :=
+def getAltName? (alt : Syntax) : Option Name :=
   let head := (getFirstAltLhs alt)[1]
   if head.isOfKind ``Parser.Term.hole then
     if head[0].isMissing then none else some `_
@@ -49,25 +48,25 @@ private def getAltName? (alt : Syntax) : Option Name :=
     let ident := head[1]
     if ident.isOfKind identKind then some ident.getId.eraseMacroScopes else none
 /-- Returns true if the the alternative is for a wildcard, and that the wildcard is not due to a syntax error. -/
-private def isAltWildcard (altStx : Syntax) : Bool :=
+def isAltWildcard (altStx : Syntax) : Bool :=
   getAltName? altStx == some `_
 /-- Returns the `inductionAlt` `ident <|> hole` -/
-private def getAltNameStx (alt : Syntax) : Syntax :=
+def getAltNameStx (alt : Syntax) : Syntax :=
   let lhs := getFirstAltLhs alt
   if lhs[1].isOfKind ``Parser.Term.hole then lhs[1] else lhs[1][1]
 /-- Return `true` if the first LHS of the given alternative contains `@`. -/
-private def altHasExplicitModifier (alt : Syntax) : Bool :=
+def altHasExplicitModifier (alt : Syntax) : Bool :=
   let lhs := getFirstAltLhs alt
   !lhs[1].isOfKind ``Parser.Term.hole && !lhs[1][0].isNone
 /-- Return the variables in the first LHS of the given alternative. -/
-private def getAltVars (alt : Syntax) : Array Syntax :=
+def getAltVars (alt : Syntax) : Array Syntax :=
   let lhs := getFirstAltLhs alt
   lhs[2].getArgs
-private def hasAltRHS (alt : Syntax) : Bool :=
+def hasAltRHS (alt : Syntax) : Bool :=
   alt[1].getNumArgs > 0
-private def getAltRHS (alt : Syntax) : Syntax :=
+def getAltRHS (alt : Syntax) : Syntax :=
   alt[1][1]
-private def getAltDArrow (alt : Syntax) : Syntax :=
+def getAltDArrow (alt : Syntax) : Syntax :=
   alt[1][0]
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
@@ -101,11 +100,11 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
         pushGoals goals
 
 /-!
-  Helper method for creating an user-defined eliminator/recursor application.
+Helper method for creating an user-defined eliminator/recursor application.
 -/
 namespace ElimApp
 
-structure Alt where
+public structure Alt where
   /-- The short name of the alternative, used in `| foo =>` cases -/
   name      : Name
   info      : ElimAltInfo
@@ -128,20 +127,20 @@ structure State where
 
 abbrev M := ReaderT Context $ StateRefT State TermElabM
 
-private def addNewArg (arg : Expr) : M Unit :=
+def addNewArg (arg : Expr) : M Unit :=
   modify fun s => { s with argPos := s.argPos+1, f := mkApp s.f arg, fType := s.fType.bindingBody!.instantiate1 arg }
 
 /-- Return the binder name at `fType`. This method assumes `fType` is a function type. -/
-private def getBindingName : M Name := return (← get).fType.bindingName!
+def getBindingName : M Name := return (← get).fType.bindingName!
 /-- Return the next argument expected type. This method assumes `fType` is a function type. -/
-private def getArgExpectedType : M Expr := return (← get).fType.bindingDomain!
+def getArgExpectedType : M Expr := return (← get).fType.bindingDomain!
 
-private def getFType : M Expr := do
+def getFType : M Expr := do
   let fType ← whnfForall (← get).fType
   modify fun s => { s with fType := fType }
   pure fType
 
-structure Result where
+public structure Result where
   elimApp     : Expr
   elimArgs    : Array Expr
   motive      : MVarId
@@ -156,7 +155,7 @@ structure Result where
   Remark: the method `addImplicitTargets` may be used to compute the sequence of implicit and
   explicit targets from the explicit ones.
 -/
-partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
+public partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
   let rec loop : M Unit := do
     match (← getFType) with
     | .forallE binderName _ _ c =>
@@ -240,7 +239,7 @@ ignores them otherwise. This limits the ability of `cases` to use unfolding func
 principles with dependent types, because after generalization of the targets, the types do
 no longer match. This can likely be improved.
 -/
-def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit := do
+public def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit := do
   let type ← inferType (mkMVar mvarId)
 
   let motiveType ← inferType (mkMVar motiveArg)
@@ -268,13 +267,13 @@ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId)
     throwError "Type mismatch when assigning motive{indentExpr motive}\n{← mkHasTypeButIsExpectedMsg motiverInferredType motiveType}"
   motiveArg.assign motive
 
-private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM Nat := do
+def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM Nat := do
   for altInfo in elimInfo.altsInfo do
     if altInfo.name == altName then
       return altInfo.numFields
   throwError "Unknown alternative name `{altName}`"
 
-private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do
+def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do
   let mut seenNames : Array Name := #[]
   let mut invalidNames : Array (Syntax × Name) := #[]
   for h : i in *...altsSyntax.size do
@@ -308,7 +307,7 @@ private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : Tacti
 /-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables,
     return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can
     be named by the user. -/
-private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do
+def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do
   let target ← altMVarId.getType
   withoutModifyingState do
     -- The `numFields` count includes explicit, implicit and let-bound variables.
@@ -320,7 +319,7 @@ private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM
     let numImplicits := (bis.filter (!·.isExplicit)).size
     return numFields - numImplicits
 
-private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TermElabM Unit :=
+def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TermElabM Unit :=
   withSaveInfoContext <| altMVarId.withContext do
     let useNamesForExplicitOnly := !altHasExplicitModifier altStx
     let mut i := 0
@@ -569,7 +568,7 @@ end ElimApp
   «induction»  := leading_parser nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> optional inductionAlts
   ```
   `stx` is syntax for `induction` or `fun_induction`. -/
-private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
+def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
   withRef stx do
     let generalizingStx :=
     if stx.getKind == ``Lean.Parser.Tactic.induction then
@@ -586,7 +585,7 @@ private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :
       getFVarIds vars
 
 -- process `generalizingVars` subterm of induction Syntax `stx`.
-private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) (elimExpr : Expr) : TacticM (Array FVarId × MVarId) :=
+def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) (elimExpr : Expr) : TacticM (Array FVarId × MVarId) :=
   mvarId.withContext do
     let userFVarIds ← getUserGeneralizingFVarIds stx
     let forbidden1 ← mkGeneralizationForbiddenSet targets
@@ -611,7 +610,7 @@ syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
 ```
 Return an array containing its alternatives.
 -/
-private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
+def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
   inductionAlts[2].getArgs
 
 /--
@@ -622,7 +621,7 @@ syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
 runs `cont (some alts)` where `alts` is an array containing all `inductionAlt`s while disabling incremental
 reuse if any other syntax changed. If there's no `with` clause, then runs `cont none`.
 -/
-private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
+def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
     (cont : Option (Array Syntax) → TacticM α) : TacticM α :=
   Term.withNarrowedTacticReuse (stx := optInductionAlts) (fun optInductionAlts =>
     if optInductionAlts.isNone then
@@ -642,21 +641,21 @@ private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
       else                                 -- has `with` clause, but no alts
         cont (some #[]))
 
-private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
+def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
   if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
 
 /--
 Returns true if the `Lean.Parser.Tactic.inductionAlt` either has more than one alternative
 or has no RHS.
 -/
-private def shouldExpandAlt (alt : Syntax) : Bool :=
+def shouldExpandAlt (alt : Syntax) : Bool :=
   alt[0].getNumArgs > 1 || (1 < alt.getNumArgs && alt[1].getNumArgs == 0)
 
 /--
 Returns `some #[alt_1, ..., alt_n]` if `alt` has multiple LHSs or if `alt` has no RHS.
 If there is no RHS, it is filled in with a hole.
 -/
-private def expandAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
+def expandAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
   if shouldExpandAlt alt then
     some <| alt[0].getArgs.map fun lhs =>
       let alt := alt.setArg 0 (mkNullNode #[lhs])
@@ -677,7 +676,7 @@ In the new `inductionAlts'` all alternatives have a single LHS.
 
 Remark: the `RHS` of alternatives with multi LHSs is copied.
 -/
-private def expandInductionAlts? (inductionAlts : Syntax) : Option Syntax := Id.run do
+def expandInductionAlts? (inductionAlts : Syntax) : Option Syntax := Id.run do
   let alts := getAltsOfInductionAlts inductionAlts
   if alts.any shouldExpandAlt then
     let mut altsNew := #[]
@@ -690,7 +689,7 @@ private def expandInductionAlts? (inductionAlts : Syntax) : Option Syntax := Id.
   else
     none
 
-private def inductionAltsPos (stx : Syntax) : Nat :=
+def inductionAltsPos (stx : Syntax) : Nat :=
   if stx.getKind == ``Lean.Parser.Tactic.induction then
     4
   else if stx.getKind == ``Lean.Parser.Tactic.cases then
@@ -710,7 +709,7 @@ syntax "induction " term,+ (" using " ident)?  ("generalizing " (colGt term:max)
 if `inductionAlts` has an alternative with multiple LHSs, and likewise for
 `cases`, `fun_induction`, `fun_cases`.
 -/
-private def expandInduction? (induction : Syntax) : Option Syntax := do
+def expandInduction? (induction : Syntax) : Option Syntax := do
   let inductionAltsPos := inductionAltsPos induction
   let optInductionAlts := induction[inductionAltsPos]
   guard <| !optInductionAlts.isNone
@@ -720,7 +719,7 @@ private def expandInduction? (induction : Syntax) : Option Syntax := do
 /--
   We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names.
   The idea is to make sure users do not write unstructured tactics. -/
-private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Unit :=
+def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Unit :=
   unless optInductionAlts.isNone do
     let mut found := false
     for alt in getAltsOfInductionAlts optInductionAlts[0] do
@@ -761,7 +760,7 @@ without turning them into MVars. So this uses `abstractMVars` at the end. This i
 It also elaborates without `heedElabAsElim` so that users can use constants that are marked
 `elabAsElim` in the `using` clause`.
 -/
-private def elabTermForElim (stx : Syntax) : TermElabM Expr := do
+def elabTermForElim (stx : Syntax) : TermElabM Expr := do
   -- Short-circuit elaborating plain identifiers
   if stx.isIdent then
     if let some e ← Term.resolveId? stx (withInfo := true) then
@@ -785,7 +784,7 @@ register_builtin_option tactic.customEliminators : Bool := {
 }
 
 -- `optElimId` is of the form `("using" term)?`
-private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
+def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
   let getBaseName? (elimName : Name) : MetaM (Option Name) := do
     -- not a precise check, but covers the common cases of T.recOn / T.casesOn
     -- as well as user defined T.myInductionOn to locate the constructors of T
@@ -825,7 +824,7 @@ where
     throwError m!"The `induction` tactic does not support the type `{name}` because it is {kind}"
         ++ .hint' "Consider using the `cases` tactic instead"
 
-private def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
+def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
   if let .fvar fvarId .. := e then
     return (← fvarId.getDecl).hasValue -- must generalize let-decls
   else
@@ -833,12 +832,12 @@ private def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
 
 
 /-- View of `Lean.Parser.Tactic.elimTarget`. -/
-structure ElimTargetView where
+public structure ElimTargetView where
   hIdent? : Option Ident
   term    : Syntax
 
 /-- Interprets a `Lean.Parser.Tactic.elimTarget`. -/
-def mkTargetView (target : Syntax) : TacticM ElimTargetView := do
+public def mkTargetView (target : Syntax) : TacticM ElimTargetView := do
   match target with
   | `(Parser.Tactic.elimTarget| $[$hIdent?:ident :]? $term) =>
     return { hIdent?, term }
@@ -900,7 +899,7 @@ def elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ide
 Generalize targets in `fun_induction` and `fun_cases`. Should behave like `elabCasesTargets` with
 no targets annotated with `h : _`.
 -/
-private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
+def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
   withMainContext do
     let exprToGeneralize ← exprs.filterM (shouldGeneralizeTarget ·)
     if exprToGeneralize.isEmpty then
@@ -941,7 +940,7 @@ def mkInitialTacticInfoForInduction (stx : Syntax) : TacticM (TacticM Info) := d
 The code path shared between `induction` and `fun_induct`; when we already have an `elimInfo`
 and the `targets` contains the implicit targets
 -/
-private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Array Expr)
+def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Array Expr)
     (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
   let mvarId ← getMainGoal
   -- save initial info before main goal is reassigned
@@ -1012,7 +1011,7 @@ def elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr := do
 /--
 Elaborates the `foo args` of `fun_induction` or `fun_cases`, returning the `ElabInfo` and targets.
 -/
-private def elabFunTarget (cases : Bool) (stx : Syntax) : TacticM (ElimInfo × Array Expr) := do
+def elabFunTarget (cases : Bool) (stx : Syntax) : TacticM (ElimInfo × Array Expr) := do
   withRef stx <| withMainContext do
     let funCall ← elabFunTargetCall cases stx
     funCall.withApp fun fn funArgs => do

src/Lean/Elab/Tactic/RCases.lean

@@ -6,11 +6,12 @@ Authors: Mario Carneiro, Jacob von Raumer
 module
 
 prelude
-public import Lean.Elab.Tactic.Induction
+public import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Induction
+import Lean.Elab.Tactic.Generalize
+import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Replace
 
-public section
-
 namespace Lean.Elab.Tactic.RCases
 open Meta Parser Tactic
 
@@ -18,18 +19,18 @@ open Meta Parser Tactic
 Enables the 'unused rcases pattern' linter. This will warn when a pattern is ignored by
 `rcases`, `rintro`, `ext` and similar tactics.
 -/
-register_option linter.unusedRCasesPattern : Bool := {
+public register_option linter.unusedRCasesPattern : Bool := {
   defValue := true
   descr := "enable the 'unused rcases pattern' linter"
 }
 
-instance : Coe Ident (TSyntax `rcasesPat) where
+public instance : Coe Ident (TSyntax `rcasesPat) where
   coe stx := Unhygienic.run `(rcasesPat| $stx:ident)
-instance : Coe (TSyntax `rcasesPat) (TSyntax ``rcasesPatMed) where
+public instance : Coe (TSyntax `rcasesPat) (TSyntax ``rcasesPatMed) where
   coe stx := Unhygienic.run `(rcasesPatMed| $stx:rcasesPat)
-instance : Coe (TSyntax ``rcasesPatMed) (TSyntax ``rcasesPatLo) where
+public instance : Coe (TSyntax ``rcasesPatMed) (TSyntax ``rcasesPatLo) where
   coe stx := Unhygienic.run `(rcasesPatLo| $stx:rcasesPatMed)
-instance : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat) where
+public instance : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat) where
   coe stx := Unhygienic.run `(rintroPat| $stx:rcasesPat)
 
 -- These frequently cause bootstrapping issues. Commented out for now, using `List/-Σ-/` and `List/-Π-/` instead.
@@ -59,7 +60,7 @@ the type being destructed, the extra patterns will match on the last element, me
 `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.
 -/
-inductive RCasesPatt : Type
+public inductive RCasesPatt : Type
   /-- A parenthesized expression, used for hovers -/
   | paren (ref : Syntax) : RCasesPatt → RCasesPatt
   /-- A named pattern like `foo` -/
@@ -266,7 +267,7 @@ This will match a pattern `pat` against a local hypothesis `e`.
   match, with updated values for `g` , `fs`, `clears`, and `a`.
 -/
 partial def rcasesCore (g : MVarId) (fs : FVarSubst) (clears : Array FVarId) (e : Expr) (a : α)
-    (pat : RCasesPatt) (cont : MVarId → FVarSubst → Array FVarId → α → TermElabM α) :
+    (pat : RCasesPatt) (cont : MVarId → FVarSubst → Array FVarId → α → Term.TermElabM α) :
     TermElabM α := do
   let asFVar : Expr → MetaM _
     | .fvar e => pure e
@@ -419,7 +420,7 @@ def generalizeExceptFVar (goal : MVarId) (args : Array GeneralizeArg) :
 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.
 -/
-def rcases (tgts : Array (Option Ident × Syntax))
+public def rcases (tgts : Array (Option Ident × Syntax))
   (pat : RCasesPatt) (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
   let pats ← match tgts.size with
   | 0 => return [g]
@@ -466,7 +467,7 @@ partial def expandRIntroPat (pat : TSyntax `rintroPat)
   | _ => acc
 
 /-- Expand a list of `rintroPat` into an equivalent list of `rcasesPat` patterns. -/
-partial def expandRIntroPats (pats : Array (TSyntax `rintroPat))
+public partial def expandRIntroPats (pats : Array (TSyntax `rintroPat))
     (acc : Array (TSyntax `rcasesPat) := #[]) (ty? : Option Term := none) :
     Array (TSyntax `rcasesPat) :=
   pats.foldl (fun acc p => expandRIntroPat p acc ty?) acc
@@ -513,7 +514,7 @@ end
 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.
 -/
-def rintro (pats : TSyntaxArray `rintroPat) (ty? : Option Term)
+public def rintro (pats : TSyntaxArray `rintroPat) (ty? : Option Term)
     (g : MVarId) : TermElabM (List MVarId) := Term.withSynthesize do
   (·.toList) <$> rintroContinue g {} #[] .missing pats ty? #[] finish