On 2012-11-25 14:37, Peter Divianszky wrote: > I guess you also considered already the automatic addition of some > hidden arguments like > > _≤_ : ℕ → ℕ → ℕ > z≤n : zero ≤ n > s≤s : m ≤ n → suc m ≤ suc n > > which would simplify the definition too. Yes, but we have not agreed on a good way to do this kind of thing. -- /NAD