From cce013731b5b355ff4528ac9717ae3e0cc5c4519 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Miyahara=20K=C5=8D?= <52843868+Komyyy@users.noreply.github.com> Date: Thu, 6 Mar 2025 07:47:35 +0900 Subject: [PATCH] doc: Fix typo (#1155) --- Batteries/Data/List/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean index a983f2a6fb..e714463a76 100644 --- a/Batteries/Data/List/Basic.lean +++ b/Batteries/Data/List/Basic.lean @@ -515,7 +515,7 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : def ofFnNthVal {n} (f : Fin n → α) (i : Nat) : Option α := if h : i < n then some (f ⟨i, h⟩) else none -/-- `disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common. -/ +/-- `Disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common. -/ def Disjoint (l₁ l₂ : List α) : Prop := ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False