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)