From 56002e1b33a7b00a0dcfe1301efbcae06bfc10d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Oct 2022 07:58:56 -0700 Subject: [PATCH] fix: fixes #1707 --- src/Lean/Elab/App.lean | 2 +- tests/lean/1707.lean | 1 + tests/lean/1707.lean.expected.out | 2 ++ 3 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 tests/lean/1707.lean create mode 100644 tests/lean/1707.lean.expected.out diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 6b2bf774c9..60df180bde 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1272,7 +1272,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra LVal.fieldName comp (toString comp.getId) none e elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc let elabFieldIdx (e idxStx : Syntax) := do - let idx := idxStx.isFieldIdx?.get! + let some idx := idxStx.isFieldIdx? | throwError "invalid field index" elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc match f with | `($(e).$idx:fieldIdx) => elabFieldIdx e idx diff --git a/tests/lean/1707.lean b/tests/lean/1707.lean new file mode 100644 index 0000000000..f34de0b48c --- /dev/null +++ b/tests/lean/1707.lean @@ -0,0 +1 @@ +def y := c.5ÿ diff --git a/tests/lean/1707.lean.expected.out b/tests/lean/1707.lean.expected.out new file mode 100644 index 0000000000..09f980e684 --- /dev/null +++ b/tests/lean/1707.lean.expected.out @@ -0,0 +1,2 @@ +1707.lean:1:9-1:12: error: invalid field index +1707.lean:1:12: error: expected command