From f05cbd1365453b7cc36eb032b5c8a8601662831e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Dec 2020 09:44:00 -0800 Subject: [PATCH] test: add test for "broken for" --- tests/lean/forErrors.lean | 6 ++++++ tests/lean/forErrors.lean.expected.out | 4 ++++ 2 files changed, 10 insertions(+) create mode 100644 tests/lean/forErrors.lean create mode 100644 tests/lean/forErrors.lean.expected.out diff --git a/tests/lean/forErrors.lean b/tests/lean/forErrors.lean new file mode 100644 index 0000000000..8d36e09410 --- /dev/null +++ b/tests/lean/forErrors.lean @@ -0,0 +1,6 @@ +def g (xs ys : List Nat) (a : α) : IO Nat := do + let mut sum := 0 + for x in xs, y in ys, c in a, z in ys do + sum := x + sum + IO.println s!"x: {x}, y: {y}, a: {a}, c: {c}, sum: {sum}" + return sum diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out new file mode 100644 index 0000000000..d815b27add --- /dev/null +++ b/tests/lean/forErrors.lean.expected.out @@ -0,0 +1,4 @@ +forErrors.lean:3:29: error: failed to synthesize instance + ToStream α ?m +forErrors.lean:5:15: error: failed to synthesize instance + ToString α