From fdd8978bfeb75af6462cf7c5cbf61548a4b8db69 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Aug 2020 15:03:49 -0700 Subject: [PATCH] fix: structure instance in patterns TODO: the structure instance `..` is not being handled correctly in patterns. We must create new pattern variables for the missing fields. Signed-off-by: Leonardo de Moura --- src/Lean/Elab/Match.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index d9336d0e61..4df18f844e 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -255,8 +255,8 @@ private partial def collect : Syntax → M Syntax let fields := (args.get! 2).getArgs; fields ← fields.mapSepElemsM fun field => do { -- parser! structInstLVal >> " := " >> termParser - newVal ← collect (field.getArg 2); - pure $ field.setArg 2 newVal + newVal ← collect (field.getArg 3); -- `structInstLVal` has arity 2 + pure $ field.setArg 3 newVal }; pure $ Syntax.node k $ args.set! 2 $ mkNullNode fields else if k == `Lean.Parser.Term.hole then do