From bf3a1e94a95394bf42d69a02ddd909ee3c3bb55c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Dec 2021 17:19:30 -0800
Subject: [PATCH] feat: add `LocalContext.foldrM`

---
 src/Lean/LocalContext.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index df0d567c51..db26a8c6e5 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -262,6 +262,11 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
     | none      => pure b
     | some decl => f b decl
 
+@[specialize] def foldrM [Monad m] (lctx : LocalContext) (f : LocalDecl → β → m β) (init : β) : m β :=
+  lctx.decls.foldrM (init := init) fun decl b => match decl with
+    | none      => pure b
+    | some decl => f decl b
+
 @[specialize] def forM [Monad m] (lctx : LocalContext) (f : LocalDecl → m PUnit) : m PUnit :=
   lctx.decls.forM fun decl => match decl with
     | none      => pure PUnit.unit
@@ -285,6 +290,9 @@ instance : ForIn m LocalContext LocalDecl where
 @[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
   Id.run <| lctx.foldlM f init start
 
+@[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β :=
+  Id.run <| lctx.foldrM f init
+
 @[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
   Id.run <| lctx.findDeclM? f