From 2a653743a112d58723cb093220fcff393cb75a4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Dec 2020 18:58:56 -0800 Subject: [PATCH] test: simple test for `deriving Inhabited` TODO: elaborate `optDeriving` suffix to `inductive/structure` commands --- tests/lean/run/derivingInhabited.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lean/run/derivingInhabited.lean diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean new file mode 100644 index 0000000000..bfa452d582 --- /dev/null +++ b/tests/lean/run/derivingInhabited.lean @@ -0,0 +1,17 @@ +inductive Foo (α : Type u) (β : Type v) where + | mk₁ : α → Foo α β + | mk₂ : List β → Foo α β + +deriving instance Inhabited for Foo + +def ex1 : Inhabited (Foo α β) := + inferInstance + +inductive Bla (α : Type u) (β : Type v) where + | mk₁ : α → Bla α β + | mk₂ : β → Bla α β + +deriving instance Inhabited for Bla + +def ex2 [Inhabited α] : Inhabited (Foo α β) := + inferInstance