chore: don't export Trans.trans

leanprover · Jan 28, 2025 · 6142fe4 · 6142fe4
1 parent eb1c9b9
commit 6142fe4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
@@ -192,10 +192,10 @@ theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
 instance : Trans (@Sublist α) Subset Subset :=
-  ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
+  ⟨fun h₁ h₂ => Trans.trans h₁.subset h₂⟩
 
 instance : Trans Subset (@Sublist α) Subset :=
-  ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩
+  ⟨fun h₁ h₂ => Trans.trans h₁ h₂.subset⟩
 
 instance : Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem :=
   ⟨fun h₁ h₂ => h₁.subset h₂⟩

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
@@ -1173,8 +1173,6 @@ class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam
   /-- Compose two proofs by transitivity, generalized over the relations involved. -/
   trans : r a b → s b c → t a c
 
-export Trans (trans)
-
 instance (r : α → γ → Sort u) : Trans Eq r r where
   trans heq h' := heq ▸ h'