Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

avoid warnings emitted by Coq #76

Open
wants to merge 3 commits into
base: coq-master
Choose a base branch
from
Open

avoid warnings emitted by Coq #76

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ec2d8bf
avoid warnings emitted by Coq
ybertot Sep 24, 2020
8b86bce
accept changes
ybertot Oct 30, 2020
648c589
changes in the shapes of graph are legitimate
ybertot Oct 30, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion tests/PrimitiveProjections.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,16 @@ Set Implicit Arguments.

Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.

Local Set Warnings "-notation-overridden".

Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.


Definition bar := @projT1.
Definition baz A P (x : @sigT A P) := projT1 x.

Definition foo (A: Type) (B: A -> Type) (C: A -> Type) (c: {x : A & {_ : B x & C x}}) : {x : A & {_ : C x & B x}}.
Definition foo (A: Type) (B: A -> Type) (C: A -> Type)
(c: { x : A & { _ : B x & C x }}) : { x : A & { _ : C x & B x }}.
Proof.
exists (projT1 c).
exists (projT2 (projT2 c)).
Expand Down
47 changes: 26 additions & 21 deletions tests/Test.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ Set Implicit Arguments.

(** ** Definitions *)

Declare Scope test_list_scope.

Section Lists.

Variable A : Type.
Expand All @@ -27,9 +29,9 @@ Section Lists.
| nil : list
| cons : A -> list -> list.

Infix "::" := cons (at level 60, right associativity) : list_scope.
Infix "::" := cons (at level 60, right associativity) : test_list_scope.

Open Scope list_scope.
Open Scope test_list_scope.

(** Head and tail *)
Definition head (l:list) :=
Expand Down Expand Up @@ -76,21 +78,21 @@ Axiom size_nil : size nil = 0.
| a :: l1 => a :: app l1 m
end.

Infix "++" := app (right associativity, at level 60) : list_scope.
Infix "++" := app (right associativity, at level 60) : test_list_scope.

End Lists.

(** Exporting list notations and tactics *)

Arguments nil {A}.
Infix "::" := cons (at level 60, right associativity) : list_scope.
Infix "++" := app (right associativity, at level 60) : list_scope.
Infix "::" := cons (at level 60, right associativity) : test_list_scope.
Infix "++" := app (right associativity, at level 60) : test_list_scope.

Open Scope list_scope.
Open Scope test_list_scope.

Delimit Scope list_scope with list.
Delimit Scope test_list_scope with lst.

Bind Scope list_scope with list.
Bind Scope test_list_scope with list.

Arguments list _%type_scope.

Expand Down Expand Up @@ -211,7 +213,7 @@ Section Facts.
now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
rewrite <- IHl; auto.
Qed.
Hint Resolve app_ass.
Hint Resolve app_ass : core.

Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
Proof.
Expand Down Expand Up @@ -412,7 +414,7 @@ Section Elts.
Proof.
unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
destruct l; simpl in |- *; [ inversion 2 | auto ].
destruct l as [| a l hl]; simpl in |- *.
destruct l as [| a l ]; simpl in |- *.
inversion 2.
intros d ie; right; apply hn; auto with arith.
Qed.
Expand Down Expand Up @@ -786,7 +788,7 @@ Section ListOps.
| perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
| perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.

Hint Constructors Permutation.
Hint Constructors Permutation : core.

(** Some facts about [Permutation] *)

Expand Down Expand Up @@ -821,7 +823,7 @@ Section ListOps.
exact perm_trans.
Qed.

Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
Hint Resolve Permutation_refl Permutation_sym Permutation_trans : core.

(** Compatibility with others operations on lists *)

Expand Down Expand Up @@ -876,7 +878,7 @@ Section ListOps.
apply perm_swap; auto.
apply perm_skip; auto.
Qed.
Hint Resolve Permutation_cons_app.
Hint Resolve Permutation_cons_app : core.

Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
Proof.
Expand Down Expand Up @@ -1075,7 +1077,7 @@ Section Map.
rewrite IHl; auto.
Qed.

Hint Constructors Permutation.
Hint Constructors Permutation : core.

Lemma Permutation_map :
forall l l', Permutation l l' -> Permutation (map l) (map l').
Expand Down Expand Up @@ -1591,19 +1593,19 @@ Section SetIncl.
Variable A : Type.

Definition incl (l m:list A) := forall a:A, In a l -> In a m.
Hint Unfold incl.
Hint Unfold incl : core.

Lemma incl_refl : forall l:list A, incl l l.
Proof.
auto.
Qed.
Hint Resolve incl_refl.
Hint Resolve incl_refl : core.

Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
Proof.
auto with datatypes.
Qed.
Hint Immediate incl_tl.
Hint Immediate incl_tl : core.

Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
Proof.
Expand All @@ -1614,13 +1616,13 @@ Section SetIncl.
Proof.
auto with datatypes.
Qed.
Hint Immediate incl_appl.
Hint Immediate incl_appl : core.

Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
Proof.
auto with datatypes.
Qed.
Hint Immediate incl_appr.
Hint Immediate incl_appr : core.

Lemma incl_cons :
forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
Expand All @@ -1635,15 +1637,15 @@ Section SetIncl.
now_show (In a0 l -> In a0 m).
auto.
Qed.
Hint Resolve incl_cons.
Hint Resolve incl_cons : core.

Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
Proof.
unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
now_show (In a n).
elim (in_app_or _ _ _ H1); auto.
Qed.
Hint Resolve incl_app.
Hint Resolve incl_app : core.

End SetIncl.

Expand Down Expand Up @@ -1733,6 +1735,8 @@ End Cutting.

Module ReDun.

Section Dummy.

Variable A : Type.

Inductive NoDup : list A -> Prop :=
Expand Down Expand Up @@ -1790,6 +1794,7 @@ Module ReDun.
destruct (NoDup_remove_2 _ _ _ H0 H).
Qed.

End Dummy.
End ReDun.


Expand Down
64 changes: 30 additions & 34 deletions tests/graph.dot.oracle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,23 @@
digraph tests/graph {
graph [ratio=0.5]
node [style=filled]
Test_removelast_app [label="removelast_app", URL=<Test.html#removelast_app>, fillcolor="#7FFFD4"] ;
Test_exists_last [label="exists_last", URL=<Test.html#exists_last>, peripheries=3, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=<Test.html#ReDun.NoDup_Permutation>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_app_removelast_last [label="app_removelast_last", URL=<Test.html#app_removelast_last>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=<Test.html#ReDun.NoDup_remove_2>, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=<Test.html#ReDun.NoDup_Permutation>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_removelast [label="removelast", URL=<Test.html#removelast>, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=<Test.html#ReDun.NoDup_remove_1>, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=<Test.html#ReDun.NoDup_remove_2>, fillcolor="#7FFFD4"] ;
Test_last [label="last", URL=<Test.html#last>, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_sind [label="NoDup_sind", URL=<Test.html#ReDun.NoDup_sind>, peripheries=3, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=<Test.html#ReDun.NoDup_remove_1>, fillcolor="#7FFFD4"] ;
Test_remove_In [label="remove_In", URL=<Test.html#remove_In>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup_sind [label="NoDup_sind", URL=<Test.html#ReDun.NoDup_sind>, peripheries=3, fillcolor="#F070D1"] ;
Test_remove [label="remove", URL=<Test.html#remove>, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_ind [label="NoDup_ind", URL=<Test.html#ReDun.NoDup_ind>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup_cons [label="NoDup_cons", URL=<Test.html#ReDun.NoDup_cons>, fillcolor="#7FAAFF"] ;
Test_remove [label="remove", URL=<Test.html#remove>, fillcolor="#F070D1"] ;
Test_ReDun_NoDup_nil [label="NoDup_nil", URL=<Test.html#ReDun.NoDup_nil>, peripheries=3, fillcolor="#7FAAFF"] ;
Test_app_nth2 [label="app_nth2", URL=<Test.html#app_nth2>, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup [label="NoDup", URL=<Test.html#ReDun.NoDup>, fillcolor="#E2CDFA"] ;
Test_ReDun_NoDup_nil [label="NoDup_nil", URL=<Test.html#ReDun.NoDup_nil>, peripheries=3, fillcolor="#7FAAFF"] ;
Test_app_nth1 [label="app_nth1", URL=<Test.html#app_nth1>, fillcolor="#7FFFD4"] ;
Test_ReDun_NoDup [label="NoDup", URL=<Test.html#ReDun.NoDup>, fillcolor="#E2CDFA"] ;
Test_nth_indep [label="nth_indep", URL=<Test.html#nth_indep>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_ReDun_A [label="A", URL=<Test.html#ReDun.A>, fillcolor="#FACDEF"] ;
Test_seq_shift [label="seq_shift", URL=<Test.html#seq_shift>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_nth_overflow [label="nth_overflow", URL=<Test.html#nth_overflow>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_seq_nth [label="seq_nth", URL=<Test.html#seq_nth>, peripheries=3, fillcolor="#7FFFD4"] ;
Expand Down Expand Up @@ -184,57 +182,52 @@ Test_count_occ_nil [label="count_occ_nil", URL=<Test.html#count_occ_nil>, periph
Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=<Test.html#count_occ_inv_nil>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_count_occ_In [label="count_occ_In", URL=<Test.html#count_occ_In>, peripheries=3, fillcolor="#7FFFD4"] ;
Test_count_occ [label="count_occ", URL=<Test.html#count_occ>, fillcolor="#F070D1"] ;
Test_removelast_app -> Test_removelast [] ;
Test_removelast_app -> Test_app [] ;
Test_removelast_app -> Test_list_ind [] ;
Test_removelast_app [label="removelast_app", URL=<Test.html#removelast_app>, fillcolor="#7FFFD4"] ;
Test_exists_last -> Test_app [] ;
Test_exists_last -> Test_list_rect [] ;
Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ;
Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ;
Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ;
Test_ReDun_NoDup_Permutation -> Test_In_split [] ;
Test_app_removelast_last -> Test_removelast [] ;
Test_app_removelast_last -> Test_last [] ;
Test_app_removelast_last -> Test_app [] ;
Test_app_removelast_last -> Test_list_ind [] ;
Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ;
Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ;
Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ;
Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ;
Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ;
Test_ReDun_NoDup_Permutation -> Test_In_split [] ;
Test_removelast -> Test_cons [] ;
Test_removelast -> Test_nil [] ;
Test_removelast -> Test_list [] ;
Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ;
Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ;
Test_last -> Test_list [] ;
Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ;
Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup [] ;
Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ;
Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ;
Test_last -> Test_list [] ;
Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ;
Test_remove_In -> Test_remove [] ;
Test_remove_In -> Test_In [] ;
Test_remove_In -> Test_list_ind [] ;
Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ;
Test_remove -> Test_cons [] ;
Test_remove -> Test_nil [] ;
Test_remove -> Test_list [] ;
Test_ReDun_NoDup_ind -> Test_ReDun_NoDup [] ;
Test_ReDun_NoDup_cons -> Test_ReDun_A [] ;
Test_ReDun_NoDup_cons -> Test_In [] ;
Test_ReDun_NoDup_cons -> Test_cons [] ;
Test_ReDun_NoDup_cons -> Test_nil [] ;
Test_remove -> Test_cons [] ;
Test_remove -> Test_nil [] ;
Test_remove -> Test_list [] ;
Test_ReDun_NoDup_nil -> Test_ReDun_A [] ;
Test_ReDun_NoDup_nil -> Test_In [] ;
Test_ReDun_NoDup_nil -> Test_cons [] ;
Test_ReDun_NoDup_nil -> Test_nil [] ;
Test_app_nth2 -> Test_nth [] ;
Test_app_nth2 -> Test_app [] ;
Test_app_nth2 -> Test_length [] ;
Test_app_nth2 -> Test_list_ind [] ;
Test_ReDun_NoDup -> Test_ReDun_A [] ;
Test_ReDun_NoDup -> Test_In [] ;
Test_ReDun_NoDup -> Test_cons [] ;
Test_ReDun_NoDup -> Test_nil [] ;
Test_ReDun_NoDup_nil -> Test_In [] ;
Test_ReDun_NoDup_nil -> Test_cons [] ;
Test_ReDun_NoDup_nil -> Test_nil [] ;
Test_app_nth1 -> Test_nth [] ;
Test_app_nth1 -> Test_app [] ;
Test_app_nth1 -> Test_length [] ;
Test_app_nth1 -> Test_list_ind [] ;
Test_ReDun_NoDup -> Test_In [] ;
Test_ReDun_NoDup -> Test_cons [] ;
Test_ReDun_NoDup -> Test_nil [] ;
Test_nth_indep -> Test_nth [] ;
Test_nth_indep -> Test_length [] ;
Test_nth_indep -> Test_list_ind [] ;
Expand Down Expand Up @@ -616,8 +609,11 @@ Test_count_occ [label="count_occ", URL=<Test.html#count_occ>, fillcolor="#F070D1
Test_count_occ_In -> Test_In [] ;
Test_count_occ_In -> Test_list_ind [] ;
Test_count_occ -> Test_list [] ;
Test_removelast_app -> Test_removelast [] ;
Test_removelast_app -> Test_app [] ;
Test_removelast_app -> Test_list_ind [] ;
subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled
subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled
Test_ReDun_A; Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; };
Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_length; Test_split_combine; Test_combine_split; Test_size; Test_in_combine_l; Test_size_nil; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_destruct_list; Test_list_prod; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_lel; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_In_dec; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_nth_in_or_default; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_nth_error; Test_seq; Test_nth_default; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; Test_removelast_app; };
Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; };
Test_removelast_app; Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_length; Test_split_combine; Test_combine_split; Test_size; Test_in_combine_l; Test_size_nil; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_destruct_list; Test_list_prod; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_lel; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_In_dec; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_nth_in_or_default; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_nth_error; Test_seq; Test_nth_default; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; };
} /* END */
Loading