@@ -19,85 +19,83 @@ public instance {α : Type u} {β : α → Type v}
1919 mkSlice carrier range := ⟨carrier.inner, range⟩
2020
2121@[simp] public theorem toList_rii {α : Type u} {β : α → Type v}
22- [Ord α] {t : Raw α β compare } : t[*...*].toList = t.toList := by
22+ (cmp : α → α → Ordering := by exact compare) {t : Raw α β cmp } : t[*...*].toList = t.toList := by
2323 apply Internal.toList_rii
2424
25- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
26- Ric.Sliceable (Raw α β cmp) α (Internal.RicSlice α β) where
27- mkSlice carrier range := ⟨carrier.inner, range⟩
28-
29- public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α]
30- {t : Raw α β compare} {wf : t.WF} {bound : α} :
31- t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by
32- apply Internal.toList_ric
33- . exact wf.out.ordered
34-
35- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
36- Rio.Sliceable (Raw α β cmp) α (Internal.RioSlice α β) where
37- mkSlice carrier range := ⟨carrier.inner, range⟩
38-
39- public theorem toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Raw α β compare} {wf : t.WF} {bound : α} :
40- t[*...<bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLT) := by
41- apply Internal.toList_rio
42- . exact wf.out.ordered
43-
44- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
45- Rci.Sliceable (Raw α β cmp) α (Internal.RciSlice α β) where
46- mkSlice carrier range := ⟨carrier.inner, range⟩
47-
48- public theorem toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Raw α β compare} {wf : t.WF} {bound : α} :
49- t[bound...*].toList = t.toList.filter (fun e => (compare e.fst bound).isGE) := by
50- apply Internal.toList_rci
51- . exact wf.out.ordered
52-
53- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
54- Rco.Sliceable (Raw α β cmp) α (Internal.RcoSlice α β) where
55- mkSlice carrier range := ⟨carrier.inner, range⟩
56-
57- public theorem toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Raw α β compare}
58- {wf : t.WF} {lowerBound upperBound : α} : t[lowerBound...<upperBound].toList =
59- t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLT) := by
60- apply Internal.toList_rco
61- . exact wf.out.ordered
62-
63- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
64- Rcc.Sliceable (Raw α β cmp) α (Internal.RccSlice α β) where
65- mkSlice carrier range := ⟨carrier.inner, range⟩
66-
67- public theorem toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Raw α β compare}
68- {wf : t.WF} {lowerBound upperBound : α} : t[lowerBound...=upperBound].toList =
69- t.toList.filter (fun e => (compare e.fst lowerBound).isGE ∧ (compare e.fst upperBound).isLE) := by
70- apply Internal.toList_rcc
71- . exact wf.out.ordered
72-
73- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
74- Roi.Sliceable (Raw α β cmp) α (Internal.RoiSlice α β) where
75- mkSlice carrier range := ⟨carrier.inner, range⟩
76-
77- public theorem toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α]
78- {t : Raw α β compare} {wf : t.WF} {bound: α} : t[bound<...*].toList =
79- t.toList.filter (fun e => (compare e.fst bound).isGT) := by
80- apply Internal.toList_roi
81- . exact wf.out.ordered
82-
83- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
84- Roc.Sliceable (Raw α β cmp) α (Internal.RocSlice α β) where
85- mkSlice carrier range := ⟨carrier.inner, range⟩
86-
87- public theorem toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Raw α β compare}
88- {wf : t.WF} {lowerBound upperBound : α} : t[lowerBound<...=upperBound].toList =
89- t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLE) := by
90- apply Internal.toList_roc
91- . exact wf.out.ordered
92-
93- public instance {α : Type u} {β : α → Type v} [Ord α] (cmp : α → α → Ordering := by exact compare) :
94- Roo.Sliceable (Raw α β cmp) α (Internal.RooSlice α β) where
95- mkSlice carrier range := ⟨carrier.inner, range⟩
96-
97- public theorem toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α]
98- {t : Raw α β compare} {wf : t.WF} {lowerBound upperBound : α} : t[lowerBound<...upperBound].toList =
99- t.toList.filter (fun e => (compare e.fst lowerBound).isGT ∧ (compare e.fst upperBound).isLT) := by
100- apply Internal.toList_roo
101- . exact wf.out.ordered
25+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
26+ Ric.Sliceable (Raw α β cmp) α (@Internal.RicSlice α β ⟨cmp⟩) :=
27+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
28+
29+ public theorem toList_ric {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
30+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
31+ t[*...=bound].toList = t.toList.filter (fun e => (cmp e.fst bound).isLE) :=
32+ @Internal.toList_ric α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) bound
33+
34+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
35+ Rio.Sliceable (Raw α β cmp) α (@Internal.RioSlice α β ⟨cmp⟩) :=
36+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
37+
38+ public theorem toList_rio {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
39+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
40+ t[*...<bound].toList = t.toList.filter (fun e => (cmp e.fst bound).isLT) :=
41+ @Internal.toList_rio α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) bound
42+
43+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
44+ Rci.Sliceable (Raw α β cmp) α (@Internal.RciSlice α β ⟨cmp⟩) :=
45+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
46+
47+ public theorem toList_rci {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
48+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
49+ t[bound...*].toList = t.toList.filter (fun e => (cmp e.fst bound).isGE) :=
50+ @Internal.toList_rci α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) bound
51+
52+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
53+ Rco.Sliceable (Raw α β cmp) α (@Internal.RcoSlice α β ⟨cmp⟩) :=
54+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
55+
56+ public theorem toList_rco {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
57+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
58+ t[lowerBound...<upperBound].toList =
59+ t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLT) :=
60+ @Internal.toList_rco α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
61+
62+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
63+ Rcc.Sliceable (Raw α β cmp) α (@Internal.RccSlice α β ⟨cmp⟩) :=
64+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
65+
66+ public theorem toList_rcc {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
67+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
68+ t[lowerBound...=upperBound].toList =
69+ t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLE) :=
70+ @Internal.toList_rcc α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
71+
72+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
73+ Roi.Sliceable (Raw α β cmp) α (@Internal.RoiSlice α β ⟨cmp⟩) :=
74+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
75+
76+ public theorem toList_roi {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
77+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound: α} : t[bound<...*].toList =
78+ t.toList.filter (fun e => (cmp e.fst bound).isGT) :=
79+ @Internal.toList_roi α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) bound
80+
81+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
82+ Roc.Sliceable (Raw α β cmp) α (@Internal.RocSlice α β ⟨cmp⟩) :=
83+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
84+
85+ public theorem toList_roc {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
86+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
87+ t[lowerBound<...=upperBound].toList =
88+ t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLE) :=
89+ @Internal.toList_roc α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
90+
91+ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare) :
92+ Roo.Sliceable (Raw α β cmp) α (@Internal.RooSlice α β ⟨cmp⟩) :=
93+ letI _ : Ord α := ⟨cmp⟩;⟨fun carrier range => ⟨carrier.inner, range⟩⟩
94+
95+ public theorem toList_roo {α : Type u} {β : α → Type v} (cmp : α → α → Ordering := by exact compare)
96+ [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {lowerBound upperBound : α} :
97+ t[lowerBound<...upperBound].toList =
98+ t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLT) :=
99+ @Internal.toList_roo α β ⟨cmp⟩ _ t.inner (@wf.out.ordered α β ⟨cmp⟩ _) lowerBound upperBound
102100
103101end Std.DTreeMap.Raw
0 commit comments