[Agda] Induction when the argument is wrapped in a constructor?

[Nils Anders Danielsson]

On Thu, Mar 20, 2008 at 8:43 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> On Thu, Mar 20, 2008 at 9:13 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw>
> wrote:
>
> > Is there a work around?
>
> I suppose you could try to unwrap. Maybe something like
>
> data Wrap : List N -> N -> Set where
>   W : forall {xs} bnd -> Wrap xs bnd
>
> f : forall {i} -> (xs : [ N ]) -> Wrap xs i -> N
> f {i} [] _ = []
> f {i} (x :: xs) (W .i) with lemma i
> ... | j with f {j} xs (W j)
>  ...     | _ = 0

Shin-Cheng, if you can describe your original problem in more detail,
then we can try to find a slightly nicer solution.

-- 
/NAD