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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2020-08-16 15:03:49 -07:00
parent bedb9d1fb6
commit fdd8978bfe

View file

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