From 5c00708b7f97ca19945216520e95f32673714801 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Sep 2022 16:32:25 -0700 Subject: [PATCH] test: specialize attribute tests --- tests/lean/specializeAttr.lean | 23 +++++++++++++++++++++ tests/lean/specializeAttr.lean.expected.out | 6 ++++++ 2 files changed, 29 insertions(+) create mode 100644 tests/lean/specializeAttr.lean create mode 100644 tests/lean/specializeAttr.lean.expected.out diff --git a/tests/lean/specializeAttr.lean b/tests/lean/specializeAttr.lean new file mode 100644 index 0000000000..735a754d81 --- /dev/null +++ b/tests/lean/specializeAttr.lean @@ -0,0 +1,23 @@ +@[specialize f g h] +def f1 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) + +@[specialize f 1 g] +def f2 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) + +@[specialize 1 f g] +def f3 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) + +@[specialize 0 g] +def f4 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) + +@[specialize 10] +def f5 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) + +@[specialize ff] +def f6 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) := + f (f (g x)) diff --git a/tests/lean/specializeAttr.lean.expected.out b/tests/lean/specializeAttr.lean.expected.out new file mode 100644 index 0000000000..1ee988d24b --- /dev/null +++ b/tests/lean/specializeAttr.lean.expected.out @@ -0,0 +1,6 @@ +specializeAttr.lean:1:17-1:18: error: invalid specialization argument name `h`, `f1` does have an argument with this name +specializeAttr.lean:5:15-5:16: error: invalid specialization argument index, `f` has already been specified as a specialization candidate +specializeAttr.lean:9:15-9:16: error: invalid specialization argument name `f`, it has already been specified as a specialization candidate +specializeAttr.lean:13:13-13:14: error: invalid specialization argument index, index must be greater than 0 +specializeAttr.lean:17:13-17:15: error: invalid argument index, `f5` has #3 arguments +specializeAttr.lean:21:13-21:15: error: invalid specialization argument name `ff`, `f6` does have an argument with this name