From 0132827d185d646f734062d72f1bce8900615e60 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 May 2024 15:20:20 +0200 Subject: [PATCH] Remove the broken test cases --- examples/test_ssreflect.v | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/examples/test_ssreflect.v b/examples/test_ssreflect.v index 07e6ce4..872fcbb 100644 --- a/examples/test_ssreflect.v +++ b/examples/test_ssreflect.v @@ -106,9 +106,6 @@ Proof. zify_op; reflexivity. Qed. Fact test_eq_op_nat n m : (n == m) = Z.eqb (Z.of_nat n) (Z.of_nat m). Proof. zify_op; reflexivity. Qed. -Fact test_addn_rec n m : Z.of_nat (n + m)%Nrec = (Z.of_nat n + Z.of_nat m)%Z. -Proof. zify_op; reflexivity. Qed. - Fact test_addn n m : Z.of_nat (n + m) = (Z.of_nat n + Z.of_nat m)%Z. Proof. zify_op; reflexivity. Qed. @@ -116,17 +113,10 @@ Fact test_addn_trec n m : Z.of_nat (NatTrec.add n m) = (Z.of_nat n + Z.of_nat m)%Z. Proof. zify_op; reflexivity. Qed. -Fact test_subn_rec n m : - Z.of_nat (n - m)%Nrec = Z.max 0 (Z.of_nat n - Z.of_nat m). -Proof. zify_op; reflexivity. Qed. - Fact test_subn n m : Z.of_nat (n - m) = Z.max 0 (Z.of_nat n - Z.of_nat m). Proof. zify_op; reflexivity. Qed. -Fact test_muln_rec n m : Z.of_nat (n * m)%Nrec = (Z.of_nat n * Z.of_nat m)%Z. -Proof. zify_op; reflexivity. Qed. - Fact test_muln n m : Z.of_nat (n * m) = (Z.of_nat n * Z.of_nat m)%Z. Proof. zify_op; reflexivity. Qed.