[Agda] how to evaluate in the current context

[Nils Anders Danielsson]

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.

-- 
/NAD