[Agda] Suspicious normalisation

[Marko Dimjašević]

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.


> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200929/7be6ef69/attachment.sig>