From d39025e343dbbeae9150fe7781f8a14220f23cd5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 20 Jan 2022 17:16:06 -0800 Subject: [PATCH] test: add test for issue #951 --- tests/lean/951.lean | 17 +++++++++++++++++ tests/lean/951.lean.expected.out | 2 ++ 2 files changed, 19 insertions(+) create mode 100644 tests/lean/951.lean create mode 100644 tests/lean/951.lean.expected.out diff --git a/tests/lean/951.lean b/tests/lean/951.lean new file mode 100644 index 0000000000..b107b0c87d --- /dev/null +++ b/tests/lean/951.lean @@ -0,0 +1,17 @@ +inductive ThingA where +| mkA +deriving Ord +instance : LE ThingA where + le a b := (compare a b).isLE + +instance (t₁ t₂ : ThingA) : Decidable (t₁ <= t₂) := inferInstance +-- TODO: we may want to suppress the name of nested instances +#check instDecidableLeThingAInstLEThingA + +inductive ThingB where +| mkB +deriving Ord +instance : LE ThingB where + le a b := (compare a b).isLE +instance (t₁ t₂ : ThingB) : Decidable (t₁ <= t₂) := inferInstance +#check instDecidableLeThingBInstLEThingB diff --git a/tests/lean/951.lean.expected.out b/tests/lean/951.lean.expected.out new file mode 100644 index 0000000000..62f2c8e85d --- /dev/null +++ b/tests/lean/951.lean.expected.out @@ -0,0 +1,2 @@ +instDecidableLeThingAInstLEThingA : (t₁ t₂ : ThingA) → Decidable (t₁ ≤ t₂) +instDecidableLeThingBInstLEThingB : (t₁ t₂ : ThingB) → Decidable (t₁ ≤ t₂)