Commit b5bf6af1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Forgot to add RationalConstruction.v

parent cd137018
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.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment