diff options
Diffstat (limited to 'src/GENERATEDIdentifiersWithoutTypes.v')
-rw-r--r-- | src/GENERATEDIdentifiersWithoutTypes.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index c250253e1..db84a33a3 100644 --- a/src/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -276,6 +276,21 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (fun x : Compilers.base.type => type.base x) (Compilers.base.type.list A) -> (fun x : Compilers.base.type => type.base x) P)%ptype + | list_rect_arrow : forall A P Q : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + ((fun x : Compilers.base.type => type.base x) A -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.list A) -> + ((fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.list A) -> + (fun x : Compilers.base.type => type.base x) P -> + (fun x : Compilers.base.type => type.base x) Q)%ptype | eager_list_rect : forall A P : Compilers.base.type, ident (((fun x : Compilers.base.type => type.base x) @@ -865,6 +880,7 @@ show_match_ident = r"""match # with | ident.eager_nat_rect P => | ident.eager_nat_rect_arrow P Q => | ident.list_rect A P => + | ident.list_rect_arrow A P Q => | ident.eager_list_rect A P => | ident.eager_list_rect_arrow A P Q => | ident.list_case A P => @@ -1475,6 +1491,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect | eager_nat_rect_arrow | list_rect + | list_rect_arrow | eager_list_rect | eager_list_rect_arrow | list_case @@ -1569,6 +1586,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => Compilers.base.type | eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type | list_rect => Compilers.base.type * Compilers.base.type + | list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type | eager_list_rect => Compilers.base.type * Compilers.base.type | eager_list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type | list_case => Compilers.base.type * Compilers.base.type @@ -1664,6 +1682,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => false | eager_nat_rect_arrow => false | list_rect => false + | list_rect_arrow => false | eager_list_rect => false | eager_list_rect_arrow => false | list_case => false @@ -1759,6 +1778,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect, Compilers.ident.eager_nat_rect P => Datatypes.Some P | eager_nat_rect_arrow, Compilers.ident.eager_nat_rect_arrow P Q => Datatypes.Some (P, Q) | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P) + | list_rect_arrow, Compilers.ident.list_rect_arrow A P Q => Datatypes.Some (A, P, Q) | eager_list_rect, Compilers.ident.eager_list_rect A P => Datatypes.Some (A, P) | eager_list_rect_arrow, Compilers.ident.eager_list_rect_arrow A P Q => Datatypes.Some (A, P, Q) | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P) @@ -1850,6 +1870,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect, _ | eager_nat_rect_arrow, _ | list_rect, _ + | list_rect_arrow, _ | eager_list_rect, _ | eager_list_rect_arrow, _ | list_case, _ @@ -1946,6 +1967,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype | eager_nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype | list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype + | list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype | eager_list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype | eager_list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype | list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype @@ -2041,6 +2063,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect => fun P => @Compilers.ident.eager_nat_rect P | eager_nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_nat_rect_arrow arg') with (P, Q) => @Compilers.ident.eager_nat_rect_arrow P Q end | list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end + | list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.list_rect_arrow A P Q end | eager_list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_list_rect arg') with (A, P) => @Compilers.ident.eager_list_rect A P end | eager_list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of eager_list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.eager_list_rect_arrow A P Q end | list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end @@ -2143,6 +2166,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => f _ (@Compilers.ident.eager_nat_rect P) | Compilers.ident.eager_nat_rect_arrow P Q => f _ (@Compilers.ident.eager_nat_rect_arrow P Q) | Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P) + | Compilers.ident.list_rect_arrow A P Q => f _ (@Compilers.ident.list_rect_arrow A P Q) | Compilers.ident.eager_list_rect A P => f _ (@Compilers.ident.eager_list_rect A P) | Compilers.ident.eager_list_rect_arrow A P Q => f _ (@Compilers.ident.eager_list_rect_arrow A P Q) | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P) @@ -2237,6 +2261,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | eager_nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype | eager_nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype | list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype + | list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype | eager_list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype | eager_list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype | list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype @@ -2331,6 +2356,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => Raw.ident.eager_nat_rect | @eager_nat_rect_arrow P Q => Raw.ident.eager_nat_rect_arrow | @list_rect A P => Raw.ident.list_rect + | @list_rect_arrow A P Q => Raw.ident.list_rect_arrow | @eager_list_rect A P => Raw.ident.eager_list_rect | @eager_list_rect_arrow A P Q => Raw.ident.eager_list_rect_arrow | @list_case A P => Raw.ident.list_case @@ -2426,6 +2452,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => [] | @eager_nat_rect_arrow P Q => [] | @list_rect A P => [] + | @list_rect_arrow A P Q => [] | @eager_list_rect A P => [] | @eager_list_rect_arrow A P Q => [] | @list_case A P => [] @@ -2521,6 +2548,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P => fun _ => @Compilers.ident.eager_nat_rect _ | @eager_nat_rect_arrow P Q => fun _ => @Compilers.ident.eager_nat_rect_arrow _ _ | @list_rect A P => fun _ => @Compilers.ident.list_rect _ _ + | @list_rect_arrow A P Q => fun _ => @Compilers.ident.list_rect_arrow _ _ _ | @eager_list_rect A P => fun _ => @Compilers.ident.eager_list_rect _ _ | @eager_list_rect_arrow A P Q => fun _ => @Compilers.ident.eager_list_rect_arrow _ _ _ | @list_case A P => fun _ => @Compilers.ident.list_case _ _ @@ -2620,6 +2648,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect P, Compilers.ident.eager_nat_rect P' => Datatypes.Some tt | @eager_nat_rect_arrow P Q, Compilers.ident.eager_nat_rect_arrow P' Q' => Datatypes.Some tt | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt + | @list_rect_arrow A P Q, Compilers.ident.list_rect_arrow A' P' Q' => Datatypes.Some tt | @eager_list_rect A P, Compilers.ident.eager_list_rect A' P' => Datatypes.Some tt | @eager_list_rect_arrow A P Q, Compilers.ident.eager_list_rect_arrow A' P' Q' => Datatypes.Some tt | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt @@ -2711,6 +2740,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @eager_nat_rect _, _ | @eager_nat_rect_arrow _ _, _ | @list_rect _ _, _ + | @list_rect_arrow _ _ _, _ | @eager_list_rect _ _, _ | @eager_list_rect_arrow _ _ _, _ | @list_case _ _, _ @@ -2807,6 +2837,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => @eager_nat_rect (base.relax P) | Compilers.ident.eager_nat_rect_arrow P Q => @eager_nat_rect_arrow (base.relax P) (base.relax Q) | Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P) + | Compilers.ident.list_rect_arrow A P Q => @list_rect_arrow (base.relax A) (base.relax P) (base.relax Q) | Compilers.ident.eager_list_rect A P => @eager_list_rect (base.relax A) (base.relax P) | Compilers.ident.eager_list_rect_arrow A P Q => @eager_list_rect_arrow (base.relax A) (base.relax P) (base.relax Q) | Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P) @@ -2902,6 +2933,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.eager_nat_rect P => tt | Compilers.ident.eager_nat_rect_arrow P Q => tt | Compilers.ident.list_rect A P => tt + | Compilers.ident.list_rect_arrow A P Q => tt | Compilers.ident.eager_list_rect A P => tt | Compilers.ident.eager_list_rect_arrow A P Q => tt | Compilers.ident.list_case A P => tt |