From 55157a31080e61823a96c38057896579750407d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Mar 2021 14:51:24 -0800
Subject: [PATCH] chore: fix test

---
 tests/lean/283.lean.expected.out | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 720d802966..2490e69737 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -1,6 +1,8 @@
-283.lean:1:4-1:5: error: fail to show termination for
-  f
-with errors
-structural recursion cannot be used
-
-well founded recursion has not been implemented yet
+283.lean:1:22-1:25: error: application type mismatch
+  f (f ?m)
+argument
+  f ?m
+has type
+  ?m : Sort ?u
+but is expected to have type
+  optParam (Sort ?u) t : Type ?u