test: add test for issue #951

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

tests/lean/951.lean.expected.out

@@ -0,0 +1,2 @@
+instDecidableLeThingAInstLEThingA : (t₁ t₂ : ThingA) → Decidable (t₁ ≤ t₂)
+instDecidableLeThingBInstLEThingB : (t₁ t₂ : ThingB) → Decidable (t₁ ≤ t₂)