Skip to content

Commit

Permalink
doc: Fix typo (#1155)
Browse files Browse the repository at this point in the history
  • Loading branch information
Komyyy authored Mar 5, 2025
1 parent b8e1430 commit cce0137
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Batteries/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit cce0137

Please sign in to comment.