Commit 88c82d21 authored by Robbert's avatar Robbert

Merge branch 'prettynat' into 'master'

Provide a pretty-printer for [nat].

See merge request robbertkrebbers/coq-stdpp!15
parents efa3890b e8560422
...@@ -347,6 +347,14 @@ Proof. ...@@ -347,6 +347,14 @@ Proof.
Qed. Qed.
Close Scope Z_scope. Close Scope Z_scope.
(** * Injectivity of casts *)
Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
(* Add others here. *)
(** * Notations and properties of [Qc] *) (** * Notations and properties of [Qc] *)
Open Scope Qc_scope. Open Scope Qc_scope.
Delimit Scope Qc_scope with Qc. Delimit Scope Qc_scope with Qc.
......
(* Copyright (c) 2012-2017, Coq-std++ developers. *) (* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export strings. From stdpp Require Export strings.
From stdpp Require Import relations. From stdpp Require Import relations numbers.
From Coq Require Import Ascii. From Coq Require Import Ascii.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -70,3 +70,7 @@ Instance pretty_Z : Pretty Z := λ x, ...@@ -70,3 +70,7 @@ Instance pretty_Z : Pretty Z := λ x,
match x with match x with
| Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x) | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
end%string. end%string.
Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
Instance pretty_nat_inj : Inj (@eq nat) (=) pretty.
Proof. apply _. Qed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment