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

fix: expandBinderType

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-09 16:47:03 -08:00
parent 04ff23f81d
commit a88fc290b4
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Init/Lean/Elab/Term.lean
View file

@ -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 `]`