feat: add isQuotRecStuck

library/Init/Lean/InductiveUtil.lean

@@ -106,7 +106,7 @@ match e.getAppFn with
     (inferType : Expr → m Expr)
     (isDefEq : Expr → Expr → m Bool)
     (env : Environment) (e : Expr) : m (Option Expr) :=
-withRec env e $ fun rec recLvls recArgs => reduceRecAux whnf inferType isDefEq env rec recLvls recArgs
+withRec env e $ reduceRecAux whnf inferType isDefEq env
 
 @[specialize] def isRecStuck {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)

library/Init/Lean/QuotUtil.lean

@@ -34,4 +34,35 @@ match rec.kind with
 | QuotKind.ind  => process 4 3
 | _             => pure none
 
+@[inline] private def withQuotRec {α} {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
+  | _ => 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
+
+@[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 =>
+  let process (majorPos : Nat) : m (Option Expr) :=
+    if h : majorPos < recArgs.size then do
+      let major := recArgs.get ⟨majorPos, h⟩;
+      major ← whnf major;
+      isStuck major
+    else
+      pure none;
+  match rec.kind with
+  | QuotKind.lift => process 5
+  | QuotKind.ind  => process 4
+  | _             => pure none
+
 end Lean