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

refactor(library): move 'filter' to init folder

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-09 17:23:28 -07:00
parent 69cc58dbda
commit 26bc1602a7
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/list/comb.lean
View file

@ -132,10 +132,6 @@ theorem length_map₂ : ∀(f : A → B → C) x y, length (map₂ f x y) = min
... = min (length (xh::xr)) (length (yh::yr)) : rfl
/- filter -/
definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
| [] := []
| (a::l) := if p a then a :: filter l else filter l
theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = [] := rfl
theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=

4
library/init/list.lean
View file

@ -65,6 +65,10 @@ definition map {B : Type} (f : A → B) : list A → list B
definition join : list (list A) → list A
| [] := []
| (l :: ls) := append l (join ls)
definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
| [] := []
| (a::l) := if p a then a :: filter l else filter l
end list
definition list_has_append [instance] {A : Type} : has_append (list A) :=