fix: bug found by getArg panic

This commit is contained in:
Sebastian Ullrich 2020-08-19 15:01:29 +02:00 committed by Leonardo de Moura
parent 4768ac2fbc
commit 203e5f76bd

View file

@ -424,7 +424,7 @@ fields ← fieldNames.foldlM
| Source.implicit _ => addField (FieldVal.term (mkHole s.ref))
| Source.explicit stx _ =>
-- stx is of the form `optional (try (termParser >> "with"))`
let src := (stx.getArg 0).getArg 0;
let src := stx.getArg 0;
let val := mkProjStx src fieldName;
addField (FieldVal.term val))
[];