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