src/Data/Rational/Literals.agda


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
35

------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational Literals
------------------------------------------------------------------------

module Data.Rational.Literals where

open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Data.Unit
open import Data.Nat
open import Data.Nat.Coprimality
open import Data.Integer
open import Data.Rational
open import Relation.Nullary.Decidable

fromℤ : ℤ → ℚ
fromℤ z = record
  { numerator     = z
  ; denominator-1 = zero
  ; isCoprime     = fromWitness (λ {i} → sym (1-coprimeTo ∣ z ∣))
  }

number : Number ℚ
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ n → fromℤ (+ n)
  }

negative : Negative ℚ
negative = record
  { Constraint = λ _ → ⊤
  ; fromNeg    = λ n → fromℤ (- (+ n))
  }