From 2b610e929327edcb8fb5a2c08fb4615a487394b5 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 9 Nov 2020 20:34:47 +0100 Subject: [PATCH] Test cases for `pretty` of `N`, `nat`, and `Z`. --- tests/pretty.ref | 0 tests/pretty.v | 62 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+) create mode 100644 tests/pretty.ref create mode 100644 tests/pretty.v diff --git a/tests/pretty.ref b/tests/pretty.ref new file mode 100644 index 00000000..e69de29b diff --git a/tests/pretty.v b/tests/pretty.v new file mode 100644 index 00000000..8557d8fe --- /dev/null +++ b/tests/pretty.v @@ -0,0 +1,62 @@ +From stdpp Require Import pretty. + +Section N. + Local Open Scope N_scope. + + Lemma pretty_N_0 : pretty 0 = "0". + Proof. reflexivity. Qed. + Lemma pretty_N_1 : pretty 1 = "1". + Proof. reflexivity. Qed. + Lemma pretty_N_9 : pretty 9 = "9". + Proof. reflexivity. Qed. + Lemma pretty_N_10 : pretty 10 = "10". + Proof. reflexivity. Qed. + Lemma pretty_N_100 : pretty 100 = "100". + Proof. reflexivity. Qed. + Lemma pretty_N_123456789 : pretty 123456789 = "123456789". + Proof. reflexivity. Qed. +End N. + +Section nat. + Local Open Scope nat_scope. + + Lemma pretty_nat_0 : pretty 0 = "0". + Proof. reflexivity. Qed. + Lemma pretty_nat_1 : pretty 1 = "1". + Proof. reflexivity. Qed. + Lemma pretty_nat_9 : pretty 9 = "9". + Proof. reflexivity. Qed. + Lemma pretty_nat_10 : pretty 10 = "10". + Proof. reflexivity. Qed. + Lemma pretty_nat_100 : pretty 100 = "100". + Proof. reflexivity. Qed. + Lemma pretty_nat_1234 : pretty 1234 = "1234". + Proof. reflexivity. Qed. +End nat. + +Section Z. + Local Open Scope Z_scope. + + Lemma pretty_Z_0 : pretty 0 = "0". + Proof. reflexivity. Qed. + Lemma pretty_Z_1 : pretty 1 = "1". + Proof. reflexivity. Qed. + Lemma pretty_Z_9 : pretty 9 = "9". + Proof. reflexivity. Qed. + Lemma pretty_Z_10 : pretty 10 = "10". + Proof. reflexivity. Qed. + Lemma pretty_Z_100 : pretty 100 = "100". + Proof. reflexivity. Qed. + Lemma pretty_Z_123456789 : pretty 123456789 = "123456789". + Proof. reflexivity. Qed. + Lemma pretty_Z_opp_1 : pretty (-1) = "-1". + Proof. reflexivity. Qed. + Lemma pretty_Z_opp_9 : pretty (-9) = "-9". + Proof. reflexivity. Qed. + Lemma pretty_Z_opp_10 : pretty (-10) = "-10". + Proof. reflexivity. Qed. + Lemma pretty_Z_opp_100 : pretty (-100) = "-100". + Proof. reflexivity. Qed. + Lemma pretty_Z_opp_123456789 : pretty (-123456789) = "-123456789". + Proof. reflexivity. Qed. +End Z. \ No newline at end of file -- GitLab