We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 83c2127 commit fe870d6Copy full SHA for fe870d6
src/Std/Data/DTreeMap/Internal/Slice.lean
@@ -633,7 +633,7 @@ def instProductivenessRelation : ProductivenessRelation (RxcIterator α β cmp)
633
split at val_eq <;> contradiction
634
635
@[no_expose]
636
-public instance instProductive : Productive (RxcIterator α β cmp) Id :=
+public instance RxcIterator.instProductive : Productive (RxcIterator α β cmp) Id :=
637
.of_productivenessRelation instProductivenessRelation
638
639
end Rxc
0 commit comments