[Agda] failure of reduction inside an abstract block

[Paolo Capriotti]

On Tue, Feb 26, 2013 at 9:19 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Well, in your example, f does not reduce in the type of g, because the type
> of g is not abstract, only the definition of g.  (Keyword abstract only
> applies to definitions, not to type signatures.)  Abstract definitions only
> reduce in other abstract things.
>
> If f is not the identity, then the type of g is ill-formed.  So, if f would
> reduce in the type of g, then the type of g would be ill-formed outside of
> the abstract block.  This is not desired.

Oh, I see. That makes sense, thank you.

BR,
Paolo