[Agda] Data.Rational

[Andreas Abel]

PLEASE, always submit self-contained examples, in this case with the 
necessary import statements:

   open import Relation.Nullary.Decidable
   open import Data.Integer
   open import Data.Nat as ℕ
   open import Data.Rational as ℚ

Agda's type-checker is incomplete when it has to handle types with 
leading hidden quantification, such as the ones of Coprime m n and c.  A 
work around is to use hidden abstraction explicitly.  In your case, giving

   \ {i} -> c

works.  Not pretty, but unavoidable until we improve on the current 
heuristics.

I recorded this as a bug

   http://code.google.com/p/agda/issues/detail?id=1079

Cheers,
Andreas

P.S.: Consider adding some of your functions to the standard library 
(which is on github, pull-requests accepted).


On 11.03.2014 05:38, Amr Sabry wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/