diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean
index fdee53153a..570cf4e607 100644
--- a/src/Lean/Compiler/LCNF/Probing.lean
+++ b/src/Lean/Compiler/LCNF/Probing.lean
@@ -127,6 +127,9 @@ def toString [ToString α] : Probe α String :=
 @[inline]
 def count : Probe α Nat := fun data => return #[data.size]
 
+@[inline]
+def sum : Probe Nat Nat := fun data => return #[data.foldl (init := 0) (·+·)]
+
 def runOnModule (moduleName : Name) (probe : Probe Decl β) (phase : Phase := Phase.base): CoreM (Array β) := do
   let ext := getExt phase
   let env ← getEnv
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 67bba6bcc7..21b098d19b 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -142,6 +142,21 @@ def isNum : Name → Bool
   | num .. => true
   | _      => false
 
+/--
+Return `true` if `n` contains a string part `s` that satifies `f`.
+
+Examples:
+```
+#eval (`foo.bla).anyS (·.startsWith "fo") -- true
+#eval (`foo.bla).anyS (·.startsWith "boo") -- false
+```
+-/
+def anyS (n : Name) (f : String → Bool) : Bool :=
+  match n with
+  | .str p s => f s || p.anyS f
+  | .num p _ => p.anyS f
+  | _ => false
+
 end Name
 end Lean