[Agda] Auto

[Wolfgang Jeltsch]

Hello,

I’m trying out Agda’s Auto function, but I’m little successful with it.
The docs on <http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto>
say that Auto is able to generate the complete implementation of map.
However, this doesn’t work for me. I tried something like this:

    data List (A : Set) : ℕ → Set where
      []  :                       List A zero
      _∷_ : ∀ {ℓ} → A → List A ℓ → List A (suc ℓ)

    infixr 5 _∷_

    map : ∀ {A A' ℓ} → (A → A') → List A ℓ → List A' ℓ
    map f xs = {!-c!}

Any ideas about what could be wrong?

Best wishes,
Wolfgang