From 74686a149a04c3b2558c910c36ab7580f1e79978 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Dec 2020 08:35:27 -0800
Subject: [PATCH] test: add `structure` field default value test

---
 tests/lean/structDefault.lean              | 11 +++++++++++
 tests/lean/structDefault.lean.expected.out |  6 ++++++
 2 files changed, 17 insertions(+)
 create mode 100644 tests/lean/structDefault.lean
 create mode 100644 tests/lean/structDefault.lean.expected.out

diff --git a/tests/lean/structDefault.lean b/tests/lean/structDefault.lean
new file mode 100644
index 0000000000..40d549ef34
--- /dev/null
+++ b/tests/lean/structDefault.lean
@@ -0,0 +1,11 @@
+structure A where
+  f : Nat → Nat → Nat
+
+structure B extends A where
+  f (a b : Nat) := 10
+
+structure C extends A where
+  f a b := 0
+
+structure D extends A where
+  f a b := true -- error
diff --git a/tests/lean/structDefault.lean.expected.out b/tests/lean/structDefault.lean.expected.out
new file mode 100644
index 0000000000..ac18a5414b
--- /dev/null
+++ b/tests/lean/structDefault.lean.expected.out
@@ -0,0 +1,6 @@
+structDefault.lean:11:11: error: type mismatch
+  true
+has type
+  Bool
+but is expected to have type
+  Nat