From aeeaaa6efc6a2ee118f77044f09d18bea5a7fc50 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 19 Jul 2022 14:24:21 +1000
Subject: [PATCH] feat: size of a LocalContext

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

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index a3290c47df..f82ffda85a 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -318,6 +318,9 @@ instance : ForIn m LocalContext LocalDecl where
 @[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β :=
   Id.run <| lctx.foldrM f init
 
+def size (lctx : LocalContext) : Nat :=
+  lctx.foldl (fun n _ => n+1) 0
+
 @[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
   Id.run <| lctx.findDeclM? f