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