[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-06 10:03, Andreas Abel wrote:
> How would you translate away the patterns in Thorsten's example?

I think recursive records should be disallowed, so this example is
irrelevant (from my perspective).

However, let's see if we can perform the translation using the case
trees that Agda uses internally.

> append : ∀ {A} → List A → List A → List A
> append (list true h t) bs = list true h (λ _ → append (t _) bs)
> append (list false _ _) bs = bs

Case tree translation (note that this isn't valid Agda surface syntax,
and doesn't type check without something like smart case):

   append : ∀ {A} → List A → List A → List A
   append as bs =
     case as of
       list b h t → case b of
         true  → list true h (λ _ → append (t _) bs)
         false → bs

After record patterns have been removed:

   append : ∀ {A} → List A → List A → List A
   append as bs =
     case isCons as of
       true  → list true (hd as) (λ _ → append (tl as _) bs)
       false → bs

With your recent changes to the termination checker the first variant of
append is accepted only if the last variant is OK, if I understand
things correctly.

-- 
/NAD