blob: 547e74b7efda6cae2f9dcd0cfe471a417f0ab4cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
(* $Id: QMake_base.v 10964 2008-05-22 11:08:13Z letouzey $ *)
(** * An implementation of rational numbers based on big integers *)
Require Export BigN.
Require Export BigZ.
(* Basic type for Q: a Z or a pair of a Z and an N *)
Inductive q_type :=
| Qz : BigZ.t -> q_type
| Qq : BigZ.t -> BigN.t -> q_type.
Definition print_type x :=
match x with
| Qz _ => Z
| _ => (Z*Z)%type
end.
Definition print x :=
match x return print_type x with
| Qz zx => BigZ.to_Z zx
| Qq nx dx => (BigZ.to_Z nx, BigN.to_Z dx)
end.
|
