max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/data): remove redundent decidable_eq instances

Browse source
This commit is contained in:
Joe Hendrix 2017-01-06 09:49:50 -08:00 • committed by Leonardo de Moura
parent 5bc5013f16
commit 767ac42dfe
2 changed files with 0 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
library/data/list/basic.lean
View file

@ -62,25 +62,4 @@ theorem length_firstn
... = min (succ n) (succ (length l))
: eq.symm (nat.min_succ_succ n (length l))
/- decidable -/
definition has_decidable_eq [h : decidable_eq α]
: ∀ (x y : list α), decidable (x = y)
| nil nil := is_true rfl
| nil (cons b s) := is_false (λ q, list.no_confusion q)
| (cons a r) nil := is_false (λ q, list.no_confusion q)
| (cons a r) (cons b s) :=
match h a b with
| (is_true h₁) :=
match has_decidable_eq r s with
| (is_true h₂) :=
is_true (calc a :: r = b :: r : congr_arg (λc, c :: r) h₁
... = b :: s : congr_arg (λt, b :: t) h₂)
| (is_false h₂) :=
is_false (λ q, list.no_confusion q (λ heq teq, h₂ teq))
end
| (is_false h₁) :=
is_false (λ q, list.no_confusion q (λ heq teq, h₁ heq))
end
end list

12
library/data/tuple.lean
View file

@ -47,14 +47,6 @@ theorem tail_cons (a : α) : Π (v : tuple α n), tail (a :: v) = v
definition to_list : tuple α n → list α | ⟨ l, h ⟩ := l
definition has_decidable_eq [decidable_eq α] {n:ℕ}
: ∀ (x y : tuple α n), decidable (x = y)
| ⟨s,p⟩ ⟨t,q⟩ :=
match list.has_decidable_eq s t with
| (is_true h) := is_true (subtype.eq h)
| (is_false h) := is_false (λr, subtype.no_confusion r (λleq (peq : p == q), h leq))
end
/- append -/
definition append {n m : nat} : tuple α n → tuple α m → tuple α (n + m)
@ -129,7 +121,3 @@ section accum
end accum
end tuple
instance decide_tuple_eq {A:Type.{1}} [decidable_eq A] {n:ℕ}
: ∀ {x y : tuple A n}, decidable (x = y)
:= tuple.has_decidable_eq