# [Agda] list member error

Andreas Abel andreas.abel at ifi.lmu.de
Sun Dec 30 15:05:11 CET 2012

```On 28.12.12 7:47 PM, Serge D. Mechveliani wrote:
> data Elem {c l : Level} {A : Setoid c l} :
>         Setoid.Carrier A -> List (Setoid.Carrier A) -> Set (suc (max c l))
>
>    -- "x  is in the list  xs  by _~~_"
>    where
>    inHead : let open Setoid {{...}} in
>                      (x y : Carrier) -> x ~~ y -> (xs : List Carrier) ->
>                                                            Elem x (y :: xs)
>    inTail : let C = Setoid.Carrier A
>             in  (x y : C) -> (xs : List C) -> Elem x xs -> Elem x (y :: xs)

Agda cannot guess parameter {A} of the recursive call to Elem.  It works
if you add {A = A}.

--
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
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
module ListMem where
open import IO.Primitive
open import Data.String as String using (toCostring)
open import Level           using (Level; suc; _?_)
open import Relation.Binary using (Setoid; module Setoid)
open import Data.List       using (List; []; _?_)

data Elem {c l : Level} {A : Setoid c l} :
Setoid.Carrier A -> List (Setoid.Carrier A) -> Set (suc (_?_ c l))

-- "x  is in the list  xs  by _~~_"
where
inHead : let open Setoid {{...}} in
(x y : Carrier) -> x ? y -> (xs : List Carrier) ->
Elem x (y ? xs)
inTail : let C = Setoid.Carrier A
in  (x y : C) -> (xs : List C) -> Elem {A = A} x xs -> Elem x (y ? xs)

main : IO Unit
main = putStrLn (toCostring "done")
```