[Agda] failure of reduction inside an abstract block

Andreas Abel andreas.abel at ifi.lmu.de
Tue Feb 26 22:19:20 CET 2013

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.


On 26.02.13 5:01 PM, Paolo Capriotti wrote:
> I've stumbled upon a problem with types defined within an abstract
> block. Sometimes, they don't get normalised as I would expect. Here is a minimal
> test case:
>      module test where
>      open import Data.Nat
>      open import Relation.Binary.PropositionalEquality
>      abstract
>        f : (A : Set) → Set
>        f A = A
>        g : subst f refl 0 ≡ subst f refl 0
>        g = refl
> If I take f out of the abstract block, then it works normally. I tried both Agda
> 2.3.2 and the development version.

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list