[Agda] Beginner's Troubles With Documentation

[Nils Anders Danielsson]

On 2009-09-17 10:56, Vag Vagoff wrote:
> 1. What is exact meaning of forall keyword?

"∀ x → T" is equivalent to "(x : _) → T".

"∀ (x : A) → T" is equivalent to "(x : A) → T".

"∀ x y → T" is equivalent to "∀ x → ∀ y → T".

Etc.

> 3. What exact and complete explanation of difference between type 
> parameters and type indices [...]?

In the result type of every constructor of a data type definition the
parameters must match those given in the data type's type signature,
whereas the indices can vary.

> 4. Why @ reserved? I haven't found where @ mentioned in documentation at 
> all

Previously Agda had as patterns (as in Haskell), and they may return in
the future.

> 5. Why open and import separated into two language constructions instead 
> of one as in many other languages?

The import keyword brings names into scope qualified, and open brings
qualified names into scope unqualified.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.