diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean index adee1a5ae8..8f00843de0 100644 --- a/Lake/DSL/DeclUtil.lean +++ b/Lake/DSL/DeclUtil.lean @@ -52,6 +52,7 @@ syntax simpleBinder := ident <|> bracketedSimpleBinder abbrev SimpleBinder := TSyntax ``simpleBinder +open Lean.Parser.Term in def expandOptSimpleBinder (stx? : Option SimpleBinder) : MacroM FunBinder := do match stx? with | some stx =>