[Agda] agda semantics

[Andreas Abel]

Hi Evgeniy,

On 2/28/11 8:26 PM, Permjacov Evgeniy wrote:
> What is difference between signatures
> f : ∀ (a : Type) → OtherType     and       f : (a : Type) → OtherType  ?

None.  \forall is just notation which can be used to omit the types of 
pi-abstractions, for instance

   \forall a -> Othertype

> what is difference between definitions
> f x = x    and       f = λ x → x ?

There should be none, but in fact there is.

The first f only unfolds if applied to an argument.  The second f always 
unfolds to its definition.

Unpleasantly, this sometimes makes a difference.  See

http://code.google.com/p/agda/issues/detail?id=365

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/