[Agda] Data.Rational

[Andreas Abel]

On 23.03.2014 17:05, Mateusz Kowalczyk wrote:
> and line 24 to
>
> normalize {m} {n} {0} {_} {()} _
>
> I'm somewhat surprised 2.3.3 doesn't complain about line 24, I should
> probably upgrade.

Agda 2.3.3 allows different arities in function clause.  That's useful 
for large eliminations and copatterns, but, as a byproduct, one can 
shorten absurd clauses.

Just a matter of style, but I prefer named arguments since they are more 
robust, so that clause could be

   normalize {g = 0} {g≢0 = ()}

(But I see it is made to look like the following clauses...)

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

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

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