[Agda] Suspicious normalisation

[Guillaume Brunerie]

Den tis 29 sep. 2020 kl 19:27 skrev Marko Dimjašević <marko at dimjasevic.net>:
>
> Dear Fredrik and Guillaume,
>
> Thank you both for your replies! Now I understand the issue and I have a
> few follow-up remarks below.
>
>
> On Mon, 2020-09-28 at 10:56 +0100, Fredrik Nordvall Forsberg wrote:
> >
> > Note that the only reduction that has happened here is is that the two
> > arguments has been replaced by their definition `suc (`suc `zero); in
> > particular, the function ƛ′_⇒_ is stuck, and has not reduced, for two
> > reasons:
> >
> > 1. its first argument does not match its only defining pattern (` x);
> > 2. its implicit argument is still an unsolved meta, so its unknown if it
> > matches its only defining pattern tt yet.
>
>
> If this is the case, wouldn't it be desirable for the Emacs function
> associated with C-c C-n (namely, agda2-compute-normalised-maybe-toplevel in
> my case) to indicate to the user that the expression is stuck? There is
> another function agda2-compute-normalised-toplevel, but it gives the same
> result when ƛ′ two ⇒ two is its argument, so based on that I don't see the
> difference between the two Emacs functions.

The result of C-c C-n is always stuck, by definition.
What C-c C-n does is to reduce the given term until it can’t be
reduced anymore (= is stuck).

Best,
Guillaume

> > You can see more clearly what is going on either by toggling the display
> > of implicit arguments in the Agda menu, in which case the "normalised"
> > term is
> >
> > ƛ′_⇒_ (`suc (`suc `zero)) {_19} (`suc (`suc `zero))
> >
> > [here _19 is the unsolved meta of type ⊥]
>
>
> This unsolved meta explains it! Thank you for pointing out how to make it
> visible.
>
>
> --
> Regards,
> Marko Dimjašević <marko at dimjasevic.net>
> https://dimjasevic.net/marko
> Mastodon: https://mamot.fr/@mdimjasevic
> PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
> Learn email self-defense! https://emailselfdefense.fsf.org