From 96c9c7505af4ab7f18135dbed136d83198f640ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2014 10:12:39 -0800 Subject: [PATCH] test(tests/lean): add another sigma-type test Signed-off-by: Leonardo de Moura --- tests/lean/sig5.lean | 9 +++++++++ tests/lean/sig5.lean.expected.out | 10 ++++++++++ 2 files changed, 19 insertions(+) create mode 100644 tests/lean/sig5.lean create mode 100644 tests/lean/sig5.lean.expected.out diff --git a/tests/lean/sig5.lean b/tests/lean/sig5.lean new file mode 100644 index 000000000..f05b7cbd7 --- /dev/null +++ b/tests/lean/sig5.lean @@ -0,0 +1,9 @@ +variable vec : Nat → Type +definition vec_with_len := sig len, vec len +variable n : Nat +variable v : vec n +check tuple n, v +check (have vec_with_len : tuple n, v) +check (let v2 : vec_with_len := tuple n, v + in v2) +check (tuple vec_with_len : n, v) diff --git a/tests/lean/sig5.lean.expected.out b/tests/lean/sig5.lean.expected.out new file mode 100644 index 000000000..9193e5ce6 --- /dev/null +++ b/tests/lean/sig5.lean.expected.out @@ -0,0 +1,10 @@ + Set: pp::colors + Set: pp::unicode + Assumed: vec + Defined: vec_with_len + Assumed: n + Assumed: v +tuple n, v : ℕ ⨯ vec n +let have_expr : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in have_expr : vec_with_len +let v2 : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in v2 : vec_with_len +tuple vec_with_len : n, v : sig len : ℕ, vec len