Skip to content

Commit

Permalink
docs: capitalize List.All in it's own docstring (#7784)
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Oct 19, 2023
1 parent 20a9a01 commit 97c0e22
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/List/Defs.lean
Expand Up @@ -220,7 +220,7 @@ end mapIdxM
#align list.sublists List.sublists
#align list.forall₂ List.Forall₂

/-- `l.all₂ p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
/-- `l.All₂ p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
`List.All₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
@[simp]
def All₂ (p : α → Prop) : List α → Prop
Expand Down

0 comments on commit 97c0e22

Please sign in to comment.