From 39d777435c024a8f46edcee6e89248b86074e10a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Nov 2019 08:40:56 -0700
Subject: [PATCH] feat: add `reduceRec`

---
 library/Init/Lean/InductiveUtil.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/library/Init/Lean/InductiveUtil.lean b/library/Init/Lean/InductiveUtil.lean
index a97bfd04b1..06b7cce7a9 100644
--- a/library/Init/Lean/InductiveUtil.lean
+++ b/library/Init/Lean/InductiveUtil.lean
@@ -91,4 +91,17 @@ if h : majorIdx < recArgs.size then do
 else
   pure none
 
+/-- Reduce recursor applications. -/
+@[specialize] def reduceRec {m : Type → Type} [Monad m]
+    (whnf : Expr → m Expr)
+    (inferType : Expr → m Expr)
+    (isDefEq : Expr → Expr → m Bool)
+    (env : Environment) (e : Expr) : m (Option Expr) :=
+match e.getAppFn with
+| Expr.const recFn recLvls =>
+  match env.find recFn with
+  | some (ConstantInfo.recInfo rec) => reduceRecAux whnf inferType isDefEq env rec recLvls e.getAppArgs
+  | _ => pure none
+| _ => pure none
+
 end Lean