added interpretation for \naturals, \rationals, and \integers

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 960756abe8ba41573efc4b0c3ca8de782e3af516..f16851f016bfcc983478224574171e2f792fc0a5 100644 (file)
--- a/helm/software/matita/library/Q/q/q.ma
+++ b/helm/software/matita/library/Q/q/q.ma
@@ -21,6 +21,8 @@ inductive Q : Set \def
   | Qpos : ratio  \to Q
   | Qneg : ratio  \to Q.
 
+interpretation "Rationals" 'Q = Q.
+
 definition Qone ≝ Qpos one.
 
 definition Qopp ≝

diff --git a/helm/software/matita/library/Z/z.ma b/helm/software/matita/library/Z/z.ma
index d598b7de87e7268594ea5ab0fdd2f63dd6f9155b..31c3a7003bdffca309780ce3e38122712efe4368 100644 (file)
--- a/helm/software/matita/library/Z/z.ma
+++ b/helm/software/matita/library/Z/z.ma
@@ -20,6 +20,8 @@ inductive Z : Set \def
 | pos : nat \to Z
 | neg : nat \to Z.
 
+interpretation "Integers" 'Z = Z.
+
 definition Z_of_nat \def
 \lambda n. match n with
 [ O \Rightarrow  OZ 

diff --git a/helm/software/matita/library/nat/nat.ma b/helm/software/matita/library/nat/nat.ma
index 9fce4df76a8b3dfbd7071582202ea648676d884b..c54b41c8d71e73262c949ea5043b6ddd2c4cc5d4 100644 (file)
--- a/helm/software/matita/library/nat/nat.ma
+++ b/helm/software/matita/library/nat/nat.ma
@@ -18,6 +18,8 @@ inductive nat : Set \def
   | O : nat
   | S : nat \to nat.
 
+interpretation "Natural numbers" 'N = nat.
+
 definition pred: nat \to nat \def
  \lambda n:nat. match n with
  [ O \Rightarrow  O