blob: f82c5d25b242eb97977369b316da50c34ec94991 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Export BigN.
Require Export BigZ.
(* Basic type for Q: a Z or a pair of a Z and an N *)
Inductive q_type : Set :=
| 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.
|
