[Agda] Agda type inference oddity on functions

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Mon Sep 27 20:50:40 CEST 2010


On 2010-09-27 11:49, Alan Jeffrey wrote:
> That is, the type inference engine doesn't infer that lambda-terms or
> applied terms have function type, which seems odd to me.

For some reason the type of an abstraction is more likely to be inferred
if you write

   λ (x : _) → …

rather than

   λ x → …

I believe Ulf introduced this behaviour in preparation for something
else which hasn't been implemented (yet?).

--
/NAD



More information about the Agda mailing list