RationalConstruction.v 314 Bytes
Newer Older
1
2
3
4
5
6
7
8
Require Import Coq.QArith.QArith.
(**
  Abbreviations for construction proper rational numbers from injected natural numbers
**)
Definition negativePower base exp :Q := 1 # base^exp.

Definition rationalFromNum n unitsBehindColon exp :Q :=
  (n * (negativePower (10) unitsBehindColon) * (negativePower (2) exp))%Q.