From a88fc290b452956b3ca5cdb9b1a85b3efb2c8bce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Dec 2019 16:47:03 -0800 Subject: [PATCH] fix: `expandBinderType` --- src/Init/Lean/Elab/Term.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index aee1eaba0a..b8b980c3fb 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -192,8 +192,11 @@ do s ← get; def mkHole := mkNode `Lean.Parser.Term.hole [mkAtom "_"] -/-- Given syntax of the form (`:` term)?, return `term` if it is present, and a hole otherwise. -/ -private def expandOptType (stx : Syntax) : Syntax := +/-- Given syntax of the forms + a) (`:` term)? + b) `:` term + into `term` if it is present, or a hole if not. -/ +private def expandBinderType (stx : Syntax) : Syntax := if stx.getNumArgs == 0 then mkHole else @@ -226,15 +229,15 @@ withNode stx $ fun node => do let type := mkHole; ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default } else if k == `Lean.Parser.Term.explicitBinder then - -- `(` binderIdent+ (`:` type)? (binderDefault <|> binderTactic)? `)` + -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)` let ids := (node.getArg 1).getArgs; - let type := expandOptType (node.getArg 2); + let type := expandBinderType (node.getArg 2); -- TODO handle `binderDefault` and `binderTactic` ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default } else if k == `Lean.Parser.Term.implicitBinder then - -- `{` binderIdent+ (`:` type)? `}` + -- `{` binderIdent+ binderType `}` let ids := (node.getArg 1).getArgs; - let type := expandOptType (node.getArg 2); + let type := expandBinderType (node.getArg 2); ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit } else if k == `Lean.Parser.Term.instBinder then do -- `[` optIdent type `]`