[Agda] function parameters similar to data parameters

Nils Anders Danielsson nad at chalmers.se
Mon Nov 26 12:02:39 CET 2012


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



More information about the Agda mailing list