[Agda] Suspicious normalisation

[Guillaume Brunerie]

It seems perfectly reasonable to me that it reduces.
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.
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.

Best,
Guillaume

Den fre 25 sep. 2020 kl 13:00 skrev Marko Dimjašević <marko at dimjasevic.net>:

> Dear Agda community,
>
> I cannot understand why can an expression
>
>   ƛ′ two ⇒ two
>
> be normalised (by running C-c C-n) at all for the code snippet below. It
> normalises to:
>
>   ƛ′ `suc (`suc `zero) ⇒ (`suc (`suc `zero))
>
>
> module LambdaVar where
>
> open import Data.Bool using (Bool; true; false; T)
> open import Data.String using (String)
> open import Data.Unit using (tt)
>
> Id : Set
> Id = String
>
> infix  5  ƛ_⇒_
> infix  8  `suc_
> infix  9  `_
>
> data Term : Set where
>   `_                      :  Id → Term
>   ƛ_⇒_                    :  Id → Term → Term
>   `zero                   :  Term
>   `suc_                   :  Term → Term
>
>
> two : Term
> two = `suc `suc `zero
>
> var? : Term → Bool
> var? (` _)  =  true
> var? _      =  false
>
> ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
> ƛ′_⇒_ (` x) {tt} N = ƛ x ⇒ N
>
>
> Shouldn't it be impossible to normalise ƛ′ two ⇒ two due to the implicit
> argument to ƛ′_⇒_ that doesn't allow Term t to be anything but a variable?
>
>
> --
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200925/e94912fe/attachment.html>