Skip to content

Commit

Permalink
chore(data/list/defs): mark pairwise.nil simp to match chain.nil (#4254)
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Sep 25, 2020
1 parent 5e8d527 commit 3a591e8
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/data/list/defs.lean
Expand Up @@ -529,6 +529,8 @@ variables {R}
pairwise R (a::l) ↔ (∀ a' ∈ l, R a a') ∧ pairwise R l :=
⟨λ p, by cases p with a l n p; exact ⟨n, p⟩, λ ⟨n, p⟩, p.cons n⟩

attribute [simp] pairwise.nil

instance decidable_pairwise [decidable_rel R] (l : list α) : decidable (pairwise R l) :=
by induction l with hd tl ih; [exact is_true pairwise.nil,
exactI decidable_of_iff' _ pairwise_cons]
Expand Down

0 comments on commit 3a591e8

Please sign in to comment.