[Agda] INLINE-pragma

[Frederik Hanghøj Iversen]

I know there's an INLINE-pragma for Agda (though it's not documented here
[1]). This pragma affects compilation. I wonder if there was something akin
to this for type-checking.

When I want to close a goal with a complex type I usually spend a
considerable time defining helper functions and in particular figuring out
what type these should have. Agda of course can help me here, but often it
doesn't display the type that I want. The best type is rarely the
non-normalized *nor* fully normalized type. Ideally I would like to be able
to step up and down these types interactively. But something perhaps easier
to implement and also super helpful would be if I could e.g. mark a "type
synonym" as being completely transparent, so that it's definition would be
inlined when I ask for goal and context.

As a super small example of what I'm looking for is:

Assume I have a type-synonym `P T = A × T' and I want to close a hole of
type `P T` then `C-c C-,` should give me `Goal: A × T`. Incidentally if I
issue `C-u C-u C-c C-,` the hole will be displayed as `Σ A (λ x → T)` which
is less helpful. Granted in this case the type is easily understood - but
this is rarely the case.

[1]: http://agda.readthedocs.io/en/latest/language/pragmas.html

-- 
Regards
*Frederik Hanghøj Iversen*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180221/ae773d77/attachment.html>