diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /theories/Lists/ListTactics.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Lists/ListTactics.v')
-rw-r--r-- | theories/Lists/ListTactics.v | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v new file mode 100644 index 00000000..a3b4e647 --- /dev/null +++ b/theories/Lists/ListTactics.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*) + +Require Import BinPos. +Require Import List. + +Ltac list_fold_right fcons fnil l := + match l with + | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl) + | nil => fnil + end. + +Ltac list_fold_left fcons fnil l := + match l with + | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl + | nil => fnil + end. + +Ltac list_iter f l := + match l with + | (cons ?x ?tl) => f x; list_iter f tl + | nil => idtac + end. + +Ltac list_iter_gen seq f l := + match l with + | (cons ?x ?tl) => + let t1 _ := f x in + let t2 _ := list_iter_gen seq f tl in + seq t1 t2 + | nil => idtac + end. + +Ltac AddFvTail a l := + match l with + | nil => constr:(cons a l) + | (cons a _) => l + | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l') + end. + +Ltac Find_at a l := + let rec find n l := + match l with + | nil => fail 100 "anomaly: Find_at" + | (cons a _) => eval compute in n + | (cons _ ?l) => find (Psucc n) l + end + in find 1%positive l. + +Ltac check_is_list t := + match t with + | cons _ ?l => check_is_list l + | nil => idtac + | _ => fail 100 "anomaly: failed to build a canonical list" + end. + +Ltac check_fv l := + check_is_list l; + match type of l with + | list _ => idtac + | _ => fail 100 "anomaly: built an ill-typed list" + end. |