From 4e5a51aa2451502b7f5388f0118be8bc4e66656f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Jan 2022 16:23:26 -0800 Subject: [PATCH] chore: fix test --- tests/lean/mutwf1.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean index cc140cdd6c..dc8438c331 100644 --- a/tests/lean/mutwf1.lean +++ b/tests/lean/mutwf1.lean @@ -10,7 +10,7 @@ mutual else n end -termination_by +termination_by' invImage (fun | Sum.inl ⟨n, true⟩ => (n, 2)