From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 16 Aug 2008 07:14:26 +0000 (+0000)
Subject: added interpretation for \naturals, \rationals, and \integers
X-Git-Tag: make_still_working~4865
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13c10bcf4c938ee43746bce6fb0e160b668e374d;p=helm.git

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 960756abe..f16851f01 100644
--- 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 d598b7de8..31c3a7003 100644
--- 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 9fce4df76..c54b41c8d 100644
--- 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