[Agda] proposal with WellFounded

[Sergei Meshveliani]

Another point: what is about the performance overhead?

Is there known a simple example when the well-founded recursion by
WellFounded of Standard increases the run-time cost essentially?

--
SM


On Tue, 2018-08-21 at 14:09 +0300, Sergei Meshveliani wrote:
> (what is a correct place to submit proposals on the language?)
> 
> 
> Dear Agda developers,
> 
> I propose to add to Agda _language_ the construct of well-founded
> recursion
> 
> (see the attachment to this letter).
> 
> I believe it is easy to implement.
> The extension will preserve all the existing applied code.
> 
> The reason for adding this construct is that using the feature of
> WellFounded of Standard library complicates programs essentially.
> 
>   
> Example
> -------
> 
> [..]