UlfNorell / agda-test

Agda test
0 stars 0 forks source link

giving changes shadowed names #994

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From jmchap...@gmail.com on December 10, 2013 13:57:27

If I am in the following situation:

module Before where

x : Set → Set x = {! λ x → x !}

And I 'give' then Agda changes the 'x' in the lambda to 'x₁':

module After where

x : Set → Set x = λ x₁ → x₁

I don't want Agda to change names I have chosen myself.

Original issue: http://code.google.com/p/agda/issues/detail?id=994