From 736f119bebbda7d41ac1b613eb8fe57fbcdbb69c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Sep 2021 15:58:00 -0700
Subject: [PATCH] feat: add `FunInfo.getArity`

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

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