Agda: When inspecting a hole, the type of the goal is not reduced.

[xekoukou]

I get this :

Goal: extend ↓ .ss ≤s extend ↓ .s
————————————————————————————————————————————————————————————
ss≤s : .ss ≤s .s
.s   : SetLL .pll
.ss  : SetLL .pll
.pll : LinLogic .i
.u   : Level
.i   : Size

but putting ss≤s in the hole actually works.

The function extend is a bit odd. ( i need to learn the technical details of with abstractions).

https://github.com/xekoukou/sparrow/blob/58fd21115b00a9064a3451748a7f66e9fad611e7/agda/SetLL.agda#L738

[UlfNorell]

By default, the show goal command doesn't normalise the goal type. Prefix with C-u C-u if you want normalisation. See https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html.

[xekoukou]

I used C-c C-, and it seems to normalize the goal by default.

edit : Ok, I prefixed with C-u C-u and it did reduce it, thus C-c C-, sometimes does not reduce types.

[gallais]

C-c C-, uses the macro agda2-maybe-normalised which means it has 3 levels which correspond to different strategies:

• "naked", it simplifies the goal (it's a heuristic which does some reductions)
• prefixed with C-u it instantiates it (i.e. no reduction at all)
• prefixed with C-u C-u it normalises it fully (which can generate big goals)