notation factored, coercion commant taking terms and not only URI

[helm.git] / helm / software / matita / library / Q / q.ma

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 683ddeb8822fa04a0474d91282c951fccbe8c1ce..51b66cacc8756f9b773f52bb95ec1edb621471a6 100644 (file)
--- 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