max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add helper function

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-31 20:12:22 -07:00
parent 8c7f514a9d
commit cae045bce8
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/Init/Lean/Declaration.lean
View file

@ -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`