From 5b296cbb33ac156ab262f231acb4f6cccc432056 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 9 Aug 2019 11:10:33 +0200 Subject: [PATCH] chore(tests/lean/ll_infer_type_bug): fix partial file manually --- tests/lean/ll_infer_type_bug.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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