From cae045bce8e821241d550bbe83c0ecbc880690f6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Oct 2019 20:12:22 -0700
Subject: [PATCH] chore: add helper function

---
 library/Init/Lean/Declaration.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/Init/Lean/Declaration.lean b/library/Init/Lean/Declaration.lean
index 2425fd561d..fdf6efb9b9 100644
--- a/library/Init/Lean/Declaration.lean
+++ b/library/Init/Lean/Declaration.lean
@@ -106,11 +106,14 @@ structure RecursorVal extends ConstantVal :=
 (nparams : Nat)              -- Number of parameters
 (nindices : Nat)             -- Number of indices
 (nmotives : Nat)             -- Number of motives
-(nminor : Nat)               -- Number of minor premises
+(nminors : Nat)              -- Number of minor premises
 (rules : List RecursorRule)  -- A reduction for each Constructor
 (k : Bool)                   -- It supports K-like reduction
 (isUnsafe : Bool)
 
+def RecursorVal.getMajorIdx (v : RecursorVal) : Nat :=
+v.nparams + v.nmotives + v.nminors + v.nindices
+
 inductive QuotKind
 | type  -- `Quot`
 | ctor  -- `Quot.mk`