fact: Definition print (r : Irat) : option Number.number := let print_pos n d := if d == 1%nat then Some (Nat.to_uint n, Decimal.Nil) else let d2d5 := match prime_decomp d with | [:: (2, d2); (5, d5)] => Some (d2, d5) | [:: (2, d2)] => Some (d2, O) | [:: (5, d5)] => Some (O, d5) | _ => None end in match d2d5 with | Some (d2, d5) => let f := (2 ^ (d5 - d2) * 5 ^ (d2 - d5))%nat in let (i, f) := edivn (n * f) (d * f) in Some (Nat.to_uint i, Nat.to_uint f) | None => None end in let print_IRat nd := match nd with | (Posz n, Posz d) => match print_pos n d with | Some (i, f) => Some (Decimal.Pos i, f) | None => None end | (Negz n, Posz d) => match print_pos n.+1 d with | Some (i, f) => Some (Decimal.Neg i, f) | None => None end | (_, Negz _) => None end in match r with | IRat nd _ => match print_IRat nd with | Some (i, f) => Some (Number.Decimal (Decimal.Decimal i f)) | None => None end end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)