[Agda] implicit lambda in Development Sep.16
Sergei Meshveliani
mechvel at botik.ru
Sun Sep 18 21:30:15 CEST 2016
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
More information about the Agda
mailing list