1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
19 [ (pp n) \Rightarrow (nn n)
20 | (nn n) \Rightarrow (pp n)
21 | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
23 definition rinv : ratio \to ratio \def
27 | (frac f) \Rightarrow frac (finv f)].
29 definition Qinv : Q → Q ≝
32 [ OQ ⇒ OQ (* arbitrary value *)
33 | Qpos r ⇒ Qpos (rinv r)
34 | Qneg r ⇒ Qneg (rinv r)