[Agda] implicit lambda in Development Sep.16
Ulf Norell
ulf.norell at gmail.com
Sun Sep 18 21:47:37 CEST 2016
It's the change to eagerly insert trailing implicit argument in left-hand
sides. See
https://github.com/agda/agda/blob/stable-2.5/doc/release-notes/2-5-2.txt#L301
and
https://github.com/agda/agda/issues/2001.
The fix is simply to move the bindings of p a b to the left-hand side:
prime∣split-nz {p} {a} {b} = impl prime∣split {p} {a} {b}
/ Ulf
On Sun, Sep 18, 2016 at 9:30 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:
> Dear Agda developers,
>
> The fragment
>
> Prime∣split : Set (α= ⊔ α)
> Prime∣split = ∀ {p a b} → IsPrime p → p ∣ (a ∙ b) → p ∣ a ⊎ p ∣ b
>
> ...
>
> prime∣split-nz : NZPack0.Prime∣split
> prime∣split-nz = \ {p a b} → impl prime∣split {p} {a} {b} -- *
> where
> impl : Prime∣split → NZPack0.Prime∣split
> impl = proj₁ Prime∣split←→Prime∣split-nz
>
>
> is type-checked in Agda-2.5.1.1,
>
> and Development Agda of September 16, 2016 reports
>
> -----------
> Found an implicit lambda where an explicit lambda was expected
> when checking that the expression
> λ {p} {a} {b} → impl prime∣split {p} {a} {b} has type
> NZPack0.IsPrime .p →
> (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p)
> ((*upCMon-NZ UpCommutativeMonoid.∙ .a) .b) →
> (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .a ⊎
> (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .b
> -----------
>
> If you can guess of what is this effect, then, please, inform me
> (because I wonder, how to fix this).
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> 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/20160918/2a27d330/attachment.html
More information about the Agda
mailing list