[Agda] agda semantics

[Darius Jahandarie]

On Mon, Feb 28, 2011 at 14:26, Permjacov Evgeniy <permeakra at gmail.com> wrote:
> What is difference between signatures
> f : ∀ (a : Type) → OtherType     and       f : (a : Type) → OtherType  ?

Nothing, but while we are here, it is interesting to note that there
is a difference between:

f : (a : Type) -> _ -> OtherType     and     f : Type -> _ -> OtherType

Because if the _ needs to involve a, then it would only be able to
infer it for the first case. Of course this makes sense after thinking
about it, but it is slightly strange at first glance since you don't
actually use the pi type explicitly.

-- 
Darius Jahandarie