<div dir="ltr">It seems perfectly reasonable to me that it reduces.<div>The thing is that it has an unsolved implicit argument of type Data.Empty.⊥, so there would be unsolvable yellow if you try to use this term in a consistent context, but there is no reason why that should prevent it from normalizing.</div><div>Depending on your use case, maybe you can use an instance argument instead of an implicit argument, this way it will fail instead of reducing, but work when the first argument is a variable.</div><div><br></div><div>Best,</div><div>Guillaume</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Den fre 25 sep. 2020 kl 13:00 skrev Marko Dimjašević <<a href="mailto:marko@dimjasevic.net">marko@dimjasevic.net</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Agda community,<br>
<br>
I cannot understand why can an expression<br>
<br>
  ƛ′ two ⇒ two<br>
<br>
be normalised (by running C-c C-n) at all for the code snippet below. It<br>
normalises to:<br>
<br>
  ƛ′ `suc (`suc `zero) ⇒ (`suc (`suc `zero))<br>
<br>
<br>
module LambdaVar where<br>
<br>
open import Data.Bool using (Bool; true; false; T)<br>
open import Data.String using (String)<br>
open import Data.Unit using (tt)<br>
<br>
Id : Set<br>
Id = String<br>
<br>
infix  5  ƛ_⇒_<br>
infix  8  `suc_<br>
infix  9  `_<br>
<br>
data Term : Set where<br>
  `_                      :  Id → Term<br>
  ƛ_⇒_                    :  Id → Term → Term<br>
  `zero                   :  Term<br>
  `suc_                   :  Term → Term<br>
<br>
<br>
two : Term<br>
two = `suc `suc `zero<br>
<br>
var? : Term → Bool<br>
var? (` _)  =  true<br>
var? _      =  false<br>
<br>
ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term<br>
ƛ′_⇒_ (` x) {tt} N = ƛ x ⇒ N<br>
<br>
<br>
Shouldn't it be impossible to normalise ƛ′ two ⇒ two due to the implicit<br>
argument to ƛ′_⇒_ that doesn't allow Term t to be anything but a variable?<br>
<br>
<br>
-- <br>
Regards,<br>
Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>><br>
<a href="https://dimjasevic.net/marko" rel="noreferrer" target="_blank">https://dimjasevic.net/marko</a><br>
Mastodon: <a href="https://mamot.fr/@mdimjasevic" rel="noreferrer" target="_blank">https://mamot.fr/@mdimjasevic</a><br>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA<br>
Learn email self-defense! <a href="https://emailselfdefense.fsf.org" rel="noreferrer" target="_blank">https://emailselfdefense.fsf.org</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>