feat: add matchConst helper function

library/Init/Lean/Environment.lean

@@ -543,4 +543,16 @@ do pExtDescrs ← persistentEnvExtensionsRef.get;
    pure ()
 
 end Environment
+
+/- Helper functions for accessing environment -/
+
+@[inline]
+def matchConst {α : Type} {m : Type → Type} [Monad m] (env : Environment) (e : Expr) (m₁ : Unit → m α) (m₂ : ConstantInfo → List Level → m α) : m α :=
+match e with
+| Expr.const n lvls =>
+  match env.find n with
+  | some cinfo => m₂ cinfo lvls
+  | _          => m₁ ()
+| _ => m₁ ()
+
 end Lean

library/Init/Lean/InductiveUtil.lean

@@ -91,14 +91,12 @@ if h : majorIdx < recArgs.size then do
 else
   pure none
 
-@[inline] private def withRec {α} {m : Type → Type} [Monad m] (env : Environment)
+@[inline] private def matchRecApp {α} {m : Type → Type} [Monad m] (env : Environment)
    (e : Expr) (k : RecursorVal → List Level → Array Expr → m (Option α)) : m (Option α) :=
-match e.getAppFn with
-| Expr.const recFn recLvls =>
-  match env.find recFn with
-  | some (ConstantInfo.recInfo rec) => k rec recLvls e.getAppArgs
+matchConst env e.getAppFn (fun _ => pure none) $ fun cinfo recLvls =>
+  match cinfo with
+  | ConstantInfo.recInfo rec => k rec recLvls e.getAppArgs
   | _ => pure none
-| _ => pure none
 
 /-- Reduce recursor applications. -/
 @[specialize] def reduceRec {m : Type → Type} [Monad m]
@@ -106,13 +104,13 @@ match e.getAppFn with
     (inferType : Expr → m Expr)
     (isDefEq : Expr → Expr → m Bool)
     (env : Environment) (e : Expr) : m (Option Expr) :=
-withRec env e $ reduceRecAux whnf inferType isDefEq env
+matchRecApp env e $ reduceRecAux whnf inferType isDefEq env
 
 @[specialize] def isRecStuck {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)
     (isStuck : Expr → m (Option Expr))
     (env : Environment) (e : Expr) : m (Option Expr) :=
-withRec env e $ fun rec recLvls recArgs =>
+matchRecApp env e $ fun rec recLvls recArgs =>
   if rec.k then
     -- TODO: improve this case
     pure none

library/Init/Lean/QuotUtil.lean

@@ -34,25 +34,23 @@ match rec.kind with
 | QuotKind.ind  => process 4 3
 | _             => pure none
 
-@[inline] private def withQuotRec {α} {m : Type → Type} [Monad m] (env : Environment)
+@[inline] private def matchQuotRecApp {α} {m : Type → Type} [Monad m] (env : Environment)
    (e : Expr) (k : QuotVal → List Level → Array Expr → m (Option α)) : m (Option α) :=
-match e.getAppFn with
-| Expr.const recFn recLvls =>
-  match env.find recFn with
-  | some (ConstantInfo.quotInfo rec) => k rec recLvls e.getAppArgs
+matchConst env e.getAppFn (fun _ => pure none) $ fun cinfo recLvls =>
+  match cinfo with
+  | ConstantInfo.quotInfo rec => k rec recLvls e.getAppArgs
   | _ => pure none
-| _ => pure none
 
 @[specialize] def reduceQuotRec {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)
     (env : Environment) (e : Expr) : m (Option Expr) :=
-withQuotRec env e $ reduceQuotRecAux whnf env
+matchQuotRecApp env e $ reduceQuotRecAux whnf env
 
 @[specialize] def isQuotRecStuck {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)
     (isStuck : Expr → m (Option Expr))
     (env : Environment) (e : Expr) : m (Option Expr) :=
-withQuotRec env e $ fun rec recLvls recArgs =>
+matchQuotRecApp env e $ fun rec recLvls recArgs =>
   let process (majorPos : Nat) : m (Option Expr) :=
     if h : majorPos < recArgs.size then do
       let major := recArgs.get ⟨majorPos, h⟩;