[Agda] new generalize feature, first version

[Peter Divianszky]

 >>> [...]
 >>
 >> 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.

All right, the syntax can be changed to be less confusing.


 >>      {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
 >>
 >> [...]
 >>
 >>      {x : ⊤} (p : tt ≡ x) → p ≡ p
 >
 > These two types are definitionally equal.

Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.


 > 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.

My idea would be stable in this sense.
Adding a new variable to a generalize block would be conservative, so 
more programs would be accepted and previous code would not change.

The idea is that type checking would halt with an error if not enough 
name suggestions were available.

If you don't like the current syntax then it could be changed in a way 
which also make my idea easier to implement, like

     generalize
       p : tt ≡ _{x y z}

Here we give name suggestions to generalized metas and at the same time 
one can notice that it is not like an ordinary meta. A bit less clean 
though.


On 2018-03-30 22:55, Nils Anders Danielsson wrote:
> 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.
>