Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]

[Jean-Philippe Bernardy]

>> 21. What is the difference between parameters and indices of a
>> datatype (except syntactically)? Is there something you can do with
>> one that you cannot do with the other? When should I preferre one over
>> the other?
>
>
> What is a parameter and what is an index can be inferred automatically

Would be a bit surprising: parameters are in scope of the
constructors; indices are not.

-- JP.