From 06bb9b7ea8cc168aaaaa582f2ffbd39aacff2ca6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Feb 2019 16:22:01 -0800 Subject: [PATCH] test(tests/compiler): add simple test for `expr` --- tests/compiler/expr.lean | 8 ++++++++ tests/compiler/expr.lean.expected.out | 2 ++ 2 files changed, 10 insertions(+) create mode 100644 tests/compiler/expr.lean create mode 100644 tests/compiler/expr.lean.expected.out diff --git a/tests/compiler/expr.lean b/tests/compiler/expr.lean new file mode 100644 index 0000000000..8f20c70ab7 --- /dev/null +++ b/tests/compiler/expr.lean @@ -0,0 +1,8 @@ +import init.lean.expr +open lean + +def main (xs : list string) : io uint32 := +let e := expr.app (expr.const `f []) (expr.const `a []) in +io.println' e.dbg_to_string *> +io.println' ("hash: " ++ to_string e.hash) *> +pure 0 diff --git a/tests/compiler/expr.lean.expected.out b/tests/compiler/expr.lean.expected.out new file mode 100644 index 0000000000..e7726977ff --- /dev/null +++ b/tests/compiler/expr.lean.expected.out @@ -0,0 +1,2 @@ +f a +hash: 938464039