X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=51b66cacc8756f9b773f52bb95ec1edb621471a6;hb=592b7d81b57ec66e0ee007de336e249b07ae0258;hp=683ddeb8822fa04a0474d91282c951fccbe8c1ce;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 683ddeb88..51b66cacc 100644
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -16,6 +16,8 @@ include "Z/compare.ma".
 include "Z/plus.ma".
 include "nat/factorization.ma".
 
+alias id "pp" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/1)".
+alias id "cons" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/3)".
 let rec enumerator_integral_fraction l ≝
  match l with
   [ pp n ⇒ Some ? l
@@ -57,6 +59,7 @@ let rec denominator_integral_fraction l ≝
        ]
   ].
 
+(*
 definition enumerator_of_fraction ≝
  λq.
   match q with
@@ -94,3 +97,4 @@ definition denominator ≝
    | Qpos r ⇒ denominator_of_fraction r
    | Qneg r ⇒ denominator_of_fraction r
    ].
+*)
\ No newline at end of file