diff options
| author |  forest <jforest@mourvedre.ensiie.fr> | 2013-11-20 20:02:35 +0100 |
|---|---|---|
| committer | forest <jforest@mourvedre.ensiie.fr> | 2013-11-20 21:13:28 +0100 |
| commit | 6b3af6de811201c706d7365611ac9e873435c6e6 (patch) | |
| tree | 81b1a8c7901bc171a4450d2436d0d78306f4e05c /theories | |
| parent | 7ca715e5f8a50bca7f5c4eee2c19c94956c59880 (diff) | |
Adding Acc_intro_generator in order to help computations of Function in particular
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Wf.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index c9fcb570a..9b4c62f87 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -150,3 +150,24 @@ End Well_founded_2. Notation Acc_iter := Fix_F (only parsing). (* compatibility *) Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *) + + + +(* Added by Julien Forest on 13/11/20 *) +Section Acc_generator. + Variable A : Type. + Variable R : A -> A -> Prop. + + (* *Lazily* add 2^n - 1 Acc_intro on top of wf. + Needed for fast reductions using Function and Program Fixpoint + and probably using Fix and Fix_F_2 + *) + Fixpoint Acc_intro_generator n (wf : well_founded R) := + match n with + | O => wf + | S n => fun x => Acc_intro x (fun y _ => Acc_intro_generator n (Acc_intro_generator n wf) y) + end. + + +End Acc_generator. +
\ No newline at end of file |