[Agda] Bug in record definition

[Andrea Vezzosi]

On Mon, Mar 28, 2011 at 12:58 PM, Nicolas Pouillard
<nicolas.pouillard at gmail.com> wrote:
> On Sun, 27 Mar 2011 22:10:47 +0200, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> [...]
>> The feature which I think should be removed is that Agda allows the
>> subsequent code to solve these metavariables.  Which means that the
>> *definition* of a thing is influenced behind the curtain by its *use*.
>> Conceptually very questionable.
>
> I would be in favor of this change to. At least by a flag to begin with.
> Does anybody want to keep this feature and why?

It'd be interesting to see what happens for the standard library and
other developements without this feature.