From 8ddde1443c199cbeeba59fa7cb52bb7a6e5bd90c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Jan 2021 10:30:35 -0800
Subject: [PATCH] test: sorry warning

---
 tests/lean/sorryWarning.lean              | 4 ++++
 tests/lean/sorryWarning.lean.expected.out | 1 +
 2 files changed, 5 insertions(+)
 create mode 100644 tests/lean/sorryWarning.lean
 create mode 100644 tests/lean/sorryWarning.lean.expected.out

diff --git a/tests/lean/sorryWarning.lean b/tests/lean/sorryWarning.lean
new file mode 100644
index 0000000000..64eca7b8a1
--- /dev/null
+++ b/tests/lean/sorryWarning.lean
@@ -0,0 +1,4 @@
+def f (x : Nat) : Nat :=
+  sorry
+def g (x : Nat) : Nat :=
+  f x
diff --git a/tests/lean/sorryWarning.lean.expected.out b/tests/lean/sorryWarning.lean.expected.out
new file mode 100644
index 0000000000..736756888b
--- /dev/null
+++ b/tests/lean/sorryWarning.lean.expected.out
@@ -0,0 +1 @@
+sorryWarning.lean:2:2: warning: declaration uses 'sorry'