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 c0e9549 commit 3c3bed7Copy full SHA for 3c3bed7
src/Std/Data/DTreeMap/Internal/Slice.lean
@@ -629,7 +629,6 @@ end Rcx
629
section Rcc
630
631
@[always_inline]
632
-
633
public def Rcc [Ord α] (t : Impl α β) (lower_bound : α) (upper_bound : α) : Iter (α := RxcIterator α β compare) ((a : α) × β a) :=
634
⟨RxcIterator.mk (Zipper.prependMapGE t lower_bound .done) upper_bound⟩
635
0 commit comments