[Agda] how to evaluate in the current context

[Nils Anders Danielsson]

On 2020-05-12 13:51, Thorsten Altenkirch wrote:
> Ok I can just introduce a shed
> 
> x = {!!}
> 
> and evaluate inside there but this is a bit clumsy. Isn’t there a
> better way to do this?

What context do you want to evaluate things in?

> Btw, for the same purposes I’d love to have an agda top-level! And a
> printer that evaluates conductive objects by mapping them to
> costrings…

Please open some tickets on the bug tracker.

-- 
/NAD