From d603baea70e379c5b4a245e0f1ef5f789b60a6b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Apr 2019 16:58:47 -0700 Subject: [PATCH] test(tests/compiler): add new test --- tests/compiler/strictOrSimp.lean | 11 +++++++++++ tests/compiler/strictOrSimp.lean.expected.out | 1 + 2 files changed, 12 insertions(+) create mode 100644 tests/compiler/strictOrSimp.lean create mode 100644 tests/compiler/strictOrSimp.lean.expected.out diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean new file mode 100644 index 0000000000..bccd4f1a2b --- /dev/null +++ b/tests/compiler/strictOrSimp.lean @@ -0,0 +1,11 @@ +partial def spin : Nat → Bool +| n := spin (n) + +@[inline] def C : Nat := 0 + +def f (b : Nat) := +if strictOr (C == 0) (spin b) then "hello" +else "world" + +def main (xs : List String) : IO Unit := +IO.println (f xs.head.toNat) diff --git a/tests/compiler/strictOrSimp.lean.expected.out b/tests/compiler/strictOrSimp.lean.expected.out new file mode 100644 index 0000000000..ce01362503 --- /dev/null +++ b/tests/compiler/strictOrSimp.lean.expected.out @@ -0,0 +1 @@ +hello