diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index db10b9f68b..c77d86bad6 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -75,4 +75,7 @@ def getFunInfo (fn : Expr) : MetaM FunInfo :=
 def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo :=
   getFunInfoAux fn (some nargs)
 
+def FunInfo.getArity (info : FunInfo) : Nat :=
+  info.paramInfo.size
+
 end Lean.Meta