There is too many 'x's and 'y's in this definition and this is confusing when
implementing it:
let compare (x : Nat)(y : Nat)
(P : Nat -> Nat -> Set)
(l : (x : Nat)(y : Nat) -> P x (plus x ('suc y)))
(e : (x : Nat) -> P x x)
(g : (x : Nat)(y : Nat) -> P (plus y ('suc x)) y) : P x y ;
Giving different, more informative names would help in the explanation.
Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 11:14
Original issue reported on code.google.com by
pedag...@gmail.com
on 7 Sep 2010 at 11:14