From b6d96dc0f474b60ff101de1a4333886eb9bf4350 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 28 Oct 2019 10:41:18 +0100 Subject: [PATCH] doc: elabissue for underapplied proj notation --- tests/elabissues/ProjNotation.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/elabissues/ProjNotation.lean diff --git a/tests/elabissues/ProjNotation.lean b/tests/elabissues/ProjNotation.lean new file mode 100644 index 0000000000..4296395f79 --- /dev/null +++ b/tests/elabissues/ProjNotation.lean @@ -0,0 +1,11 @@ +/- Underapplying a projection notation applies the 'this' argument to the wrong parameter. + It should either fail or (preferably) construct an explicit lambda. -/ + +-- Char → Bool +#check fun c => ['a', 'b'].elem c +-- List (List Char) → Bool +#check ['a', 'b'].elem +-- works +#check fun (s : String) => s.split (fun c => ['a', 'b'].elem c) +-- doesn't work +#check fun (s : String) => s.split (['a', 'b'].elem)