[Agda] new generalize feature, first version

[Nils Anders Danielsson]

On 2018-03-30 22:27, Peter Divianszky wrote:
>> What does the following code expand to?
>>
>> [...]
> 
> The first one.

This means that meta-variables do not have their usual meaning under
generalize. Perhaps it would be better to use a different notation for
the magic meta-variables.

>      {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
> 
> [...]
> 
>      {x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

> I also have an idea how to give predictable,
> non-automatically-generated names to hidden arguments, but that is not
> implemented yet. So both of your wishes can be fulfilled, I hope.

One property I did not bring up was that of stability. I hope that we
will not end up in a situation in which one can break lots of code by,
say, adding one variable name to a generalize block.

-- 
/NAD