[Agda] Data.Rational

[Amr Sabry]

Hi,

I need some decent Rational library and since the current Data.Rational
looks like it needs quite a bit of extension, I started writing a few
small functions. I am getting stuck very quickly though. Here is a small
example that should work:

-- unary negation
ℚ- : ℚ → ℚ
ℚ- p with ℚ.numerator p | ℚ.denominator-1 p | toWitness (ℚ.isCoprime p)
... | -[1+ n ] | d | c = (+ ℕ.suc n ÷ ℕ.suc d) {fromWitness {!!}}
... | + 0 | d | _ = p
... | + ℕ.suc n | d | c = (-[1+ n ] ÷ ℕ.suc d) {fromWitness {!!}}

In the first line, c has type:

  c  : {i : ℕ} → Σ (i ∣ ℕ.suc n) (λ x → i ∣ ℕ.suc d) → i ≡ 1

The goal is:

  ?0 : Coprime (ℕ.suc n) (ℕ.suc d)

where Coprime is defined in Data.Nat.Coprimality as:

  Coprime m n = ∀ {i} → (i ∣ m) × (i ∣ n) → (i ≡ 1)

As far as I can see, the type of the goal expands directly to the type
of c and in fact, "giving" c to the hole works but then the file doesn't
reload after that?

Any suggestions? --Amr