[Agda] new generalize feature, first version

[Nils Anders Danielsson]

On 2018-03-30 10:25, Peter Divianszky wrote:
> For example,
> 
>    generalize A {B .C} : Set
> 
> will generalize A as non-implicit, B as implicit and C as implicit an hidden.

Hidden? Do you mean irrelevant?

>  > I think that I might prefer more easily predictable types. If we skip
>  > the magic underscores, then we get that, at the cost of more verbosity:
>  >
>  >    generalize
>  >      {Γ Δ Θ} : Con
>  >      {A B}   : Ty Γ
>  >      {C}     : Ty Δ
>  >
>  > Now it is obvious what the names of the arguments are and how they are
>  > ordered: just drop the parts of the telescope that are unused.
>  >
>  > This also allows you to have regular underscores in the types:
>  >
>  >    generalize
>  >      {p} : tt ≡ _
> 
> The implementation does exactly this.
> Your examples are already valid. Both recursive generalize (like in
> your first example) and generalize with meta (like in your second
> example) is valid.

What does the following code expand to?

   generalize
     {x} : ⊤
     p   : tt ≡ _

   postulate
     foo : p ≡ p

Is it something like

   postulate
     foo : {x : ⊤} (p : tt ≡ x) → p ≡ p

or

   postulate
     foo : (p : tt ≡ tt) → p ≡ p?

Anyway, my main point was that I want it to be easy to understand what
the type of a definition is. The names of implicit arguments matter, as
does the order of arguments. When we have discussed this kind of feature
in the past some issues have come up:

* Is the order of the arguments unknown (or hard to predict)? In that
   case it should (IMO) only be possible to give them by name, not by
   position.

* Are the names automatically generated? In that case it should (IMO)
   not be possible to give the arguments by name.

If you have arguments that can neither be given by position nor by name,
then this can potentially lead to usability issues.

> I am not familiar with sections, can you point to a documentation?

https://coq.inria.fr/refman/gallina-ext.html#Section

-- 
/NAD