[Agda] Normalisation before termination checking

[Nils Anders Danielsson]

On Tue, Jul 22, 2008 at 8:06 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
> Can you explain what the exact problem is? There might be a theoretical
> problem behind this, and making a quick adhoc fix might not be the
> right solution.

Let us say that you have two guarded definitions,

  a ~ c₁ e₁ (c₂ (e₂ i) a)
  b ~ c₁ e₁ (c₂ (e₂ j) b),

where c₁ and c₂ are codata constructors, and e₁ and e₂ are arbitrarily
large expressions not involving a and b. In this case you cannot
abstract out the common part of the definitions, because the resulting
code is not guarded:

  f x y = c₁ e₁ (c₂ (e₂ x) y)
  a ~ f i a
  b ~ f j b.

-- 
/NAD