diff --git a/tests/lean/ll_infer_type_bug.lean b/tests/lean/ll_infer_type_bug.lean index ad2145ed28..cce74d258e 100644 --- a/tests/lean/ll_infer_type_bug.lean +++ b/tests/lean/ll_infer_type_bug.lean @@ -1,6 +1,6 @@ def f : List Nat → Bool -| [] := false -| (a::as) := a > 0 && f as +| [] => false +| (a::as) => a > 0 && f as #check f._main._cstage2