[Agda] how to evaluate in the current context

[Andreas Abel]

Here you go: https://github.com/agda/agda/issues/4647

Discussions continue there, please.

On 2020-05-12 17:12, Nils Anders Danielsson wrote:
> On 2020-05-12 15:54, Thorsten Altenkirch wrote:
>> That is I want to evaluate the expression as if I put it at the end of
>> the current file.
> 
> That can be ambiguous. However, let's discuss this on the bug tracker.
> 
>> I guess this is more a feature request.
> 
> Feature requests are welcome on the bug tracker.
>