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

chore: generalize withDeclId

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-10 14:07:55 -07:00
parent e26ec036ba
commit c8636f2bf7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Command.lean
View file

@ -636,7 +636,7 @@ else
let optUnivDeclStx := declId.getArg 1;
(id, optUnivDeclStx)
@[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
def withDeclId {α} (declId : Syntax) (f : Name → CommandElabM α) : CommandElabM α := do
-- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
let (id, optUnivDeclStx) := expandDeclId declId;
savedLevelNames ← getLevelNames;