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

feat: add mkRecFor

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-22 11:24:46 -08:00
parent 38cb8907a0
commit 472276f63f
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Declaration.lean
View file

@ -213,4 +213,8 @@ constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) :
constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr := arbitrary _
end ConstantInfo
def mkRecFor (declName : Name) : Name :=
mkNameStr declName "rec"
end Lean

2
src/Init/Lean/Meta/RecursorInfo.lean
View file

@ -106,7 +106,7 @@ else do
if s != "recOn" && s != "casesOn" && s != "brecOn" then
pure none
else do
recInfo ← getConstInfo (mkNameStr p "rec");
recInfo ← getConstInfo (mkRecFor p);
match recInfo with
| ConstantInfo.recInfo val => pure (some (val.nparams + val.nindices + (if s == "casesOn" then 1 else val.nmotives)))
| _ => throw $ Exception.other "unexpected recursor information"