Library Asm.Util.ListUtil
Set Implicit Arguments.
Require Import List TheoryList.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Lemma In_AllS : forall (T : Set) (f : T -> Prop) (ls : list T),
(forall x, In x ls -> f x)
-> AllS f ls.
Lemma In_dec : forall (T : Set) (eq_dec : forall (x y : T), {x = y} + {x <> y})
(x : T) ls,
{In x ls} + {~In x ls}.
Lemma AllS_dec : forall T f (ls : list T),
{AllS (fun x => f x = true) ls} + {~AllS (fun x => f x = true) ls}.
Lemma AllS_pdec : forall (T : Set) (P : T -> Prop) (f : forall x : T, pred_option (P x)) (ls : list T),
{AllS (fun x => popt_Prop (f x)) ls} + {~AllS (fun x => popt_Prop (f x)) ls}.
Lemma AllS_dec_option : forall T f (ls : list T),
pred_option (AllS (fun x => f x = true) ls).
Lemma AllS_pdec_option : forall (T : Set) (P : T -> Prop) (f : forall x : T, pred_option (P x)) (ls : list T),
pred_option (AllS (fun x => popt_Prop (f x)) ls).
Lemma AllS_In : forall T f (ls : list T),
AllS f ls
-> forall x, In x ls
-> f x.
Lemma AllS_imp : forall (T : Set) (p1 p2 : T -> Prop),
(forall x, p1 x -> p2 x)
-> forall ls,
AllS p1 ls -> AllS p2 ls.
Lemma In_map : forall (T S : Set) (f : T -> S) ls x,
In x (map f ls)
-> exists y, In y ls /\ x = f y.
Lemma In_map' : forall (T S : Set) (f : T -> S) ls x,
(exists y, In y ls /\ x = f y)
-> In x (map f ls).
Section iter.
Variable T : Set.
Variable f : T -> unit.
Fixpoint iter' (v : unit) (ls : list T) {struct ls} : unit :=
match ls with
| nil => tt
| cons x ls => iter' (f x) ls
end.
Definition iter := iter' tt.
End iter.
Index
This page has been generated by coqdoc