Skip to content

Commit

Permalink
chore(data/list/forall2): fix incorrect docstring (#14276)
Browse files Browse the repository at this point in the history
The previous docstring was false, this corrects the definition. 



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
  • Loading branch information
b-mehta and b-mehta committed May 24, 2022
1 parent 73a6125 commit ec8587f
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/data/list/forall2.lean
Expand Up @@ -9,7 +9,8 @@ import data.list.infix
# Double universal quantification on a list
This file provides an API for `list.forall₂` (definition in `data.list.defs`).
`forall₂ r l₁ l₂` means that `∀ a ∈ l₁, ∀ b ∈ l₂, r a b`, where `l₁`, `l₂` are lists.
`forall₂ R l₁ l₂` means that `l₁` and `l₂` have the same length, and whenever `a` is the nth element
of `l₁`, and `b` is the nth element of `l₂`, then `R a b` is satisfied.
-/

open nat function
Expand Down

0 comments on commit ec8587f

Please sign in to comment.