Frederik Hanghøj Iversen
2018-02-21 14:40:16 UTC
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
[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*
Regards
*Frederik HanghÞj Iversen*