-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Revert "Revert "Add example from coq/coq#16172 (#22)""
This reverts commit 19ae4cd.
- Loading branch information
1 parent
19ae4cd
commit fe99855
Showing
1 changed file
with
35 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
Module Type T. | ||
Parameter t : Type. | ||
End T. | ||
|
||
Module F (X:T). | ||
(* number of occurences determines the exponential: here 4 *) | ||
Definition t : Type := X.t * X.t * X.t * X.t. | ||
End F. | ||
|
||
Require Import Coq.extraction.Extraction. | ||
|
||
Module A0. Definition t := nat. End A0. | ||
|
||
Module A1 := F A0. | ||
Module A2 := F A1. | ||
Module A3 := F A2. | ||
Module A4 := F A3. | ||
Module A5 := F A4. | ||
Module A6 := F A5. | ||
Module A7 := F A6. | ||
Module A8 := F A7. | ||
Module A9 := F A8. | ||
|
||
Set Boolean Equality Schemes. | ||
Time Record Foo5 := { foo5 : A5.t }. (* 0.037s *) | ||
Time Record Foo6 := { foo6 : A6.t }. (* 0.06 s *) | ||
Time Record Foo7 := { foo7 : A7.t }. (* 0.248s *) | ||
Time Record Foo8 := { foo8 : A8.t }. (* 1.015s *) | ||
Time Record Foo9 := { foo9 : A9.t }. (* 3.811s *) | ||
|
||
Time Redirect "A5" Recursive Extraction A5.t. (* 0.009s *) | ||
Time Redirect "A6" Recursive Extraction A6.t. (* 0.041s *) | ||
Time Redirect "A7" Recursive Extraction A7.t. (* 0.177s *) | ||
Time Redirect "A8" Recursive Extraction A8.t. (* 0.744s *) | ||
Time Redirect "A9" Recursive Extraction A9.t. (* 3.12 s *) |