From d29d23cadeee2bd788f78fd71bedc94bee9a0a35 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2014 15:29:16 -0800 Subject: [PATCH] test(tests/lean): alias command error Signed-off-by: Leonardo de Moura --- tests/lean/alias3.lean | 2 ++ tests/lean/alias3.lean.expected.out | 3 +++ 2 files changed, 5 insertions(+) create mode 100644 tests/lean/alias3.lean create mode 100644 tests/lean/alias3.lean.expected.out diff --git a/tests/lean/alias3.lean b/tests/lean/alias3.lean new file mode 100644 index 000000000..52a0ff2c1 --- /dev/null +++ b/tests/lean/alias3.lean @@ -0,0 +1,2 @@ +alias A : Bool +alias A : Nat \ No newline at end of file diff --git a/tests/lean/alias3.lean.expected.out b/tests/lean/alias3.lean.expected.out new file mode 100644 index 000000000..2c4f79c4e --- /dev/null +++ b/tests/lean/alias3.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 2, pos: 13) alias 'A' was already defined