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

refactor: polymorphic elabAttrs and elabAttr

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-26 09:50:03 -07:00
parent 524eca4d7f
commit a413da856f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/DeclModifiers.lean
View file

@ -63,7 +63,7 @@ instance Modifiers.hasFormat : HasFormat Modifiers :=
instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
def elabAttr (stx : Syntax) : CommandElabM Attribute := do
def elabAttr {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m Attribute := do
-- rawIdent >> many attrArg
let nameStx := stx.getArg 0;
attrName ← match nameStx.isIdOrAtom? with
@ -77,7 +77,7 @@ let args := stx.getArg 1;
let args := if args.getNumArgs == 0 then Syntax.missing else args;
pure { name := attrName, args := args }
def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
def elabAttrs {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (Array Attribute) :=
(stx.getArg 1).foldSepArgsM
(fun stx attrs => do
attr ← elabAttr stx;