diff --git a/tests/lean/run/inline_fn.lean b/tests/lean/run/inline_fn.lean index 95252192da..e6636e5aa0 100644 --- a/tests/lean/run/inline_fn.lean +++ b/tests/lean/run/inline_fn.lean @@ -5,9 +5,6 @@ def h : Nat → Nat | 0 := 10 | (n+1) := n * h n -set_option pp.all true -set_option trace.compiler true - def g1 (x : Nat) := inline f x