From 13c10bcf4c938ee43746bce6fb0e160b668e374d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 16 Aug 2008 07:14:26 +0000 Subject: [PATCH] added interpretation for \naturals, \rationals, and \integers --- helm/software/matita/library/Q/q/q.ma | 2 ++ helm/software/matita/library/Z/z.ma | 2 ++ helm/software/matita/library/nat/nat.ma | 2 ++ 3 files changed, 6 insertions(+) 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 -- 2.39.2