diff options
Diffstat (limited to 'theories/Init/Wf.v')
| -rw-r--r-- | theories/Init/Wf.v | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index f46b2b11..d3f8f1ab 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 10712 2008-03-23 11:38:38Z herbelin $ i*) +(*i $Id: Wf.v 11251 2008-07-24 08:28:40Z herbelin $ i*) (** * This module proves the validity of - well-founded recursion (also known as course of values) @@ -27,6 +27,7 @@ Section Well_founded. Variable R : A -> A -> Prop. (** The accessibility predicate is defined to be non-informative *) + (** (Acc_rect is automatically defined because Acc is a singleton type) *) Inductive Acc (x: A) : Prop := Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. @@ -35,22 +36,6 @@ Section Well_founded. destruct 1; trivial. Defined. - (** Informative elimination : - [let Acc_rec F = let rec wf x = F x wf in wf] *) - - Section AccRecType. - - Variable P : A -> Type. - Variable F : forall x:A, - (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. - - Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x := - F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)). - - End AccRecType. - - Definition Acc_rec (P:A -> Set) := Acc_rect P. - (** A relation is well-founded if every element is accessible *) Definition well_founded := forall a:A, Acc a. |