Using List remove function
coq
Solution
`remove` is defined in a context containing:
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
The function removes takes this as a first argument (which you can see by doing `Print remove.`)
This hypothesis is a function deciding equality of elements of the type in your list. In your case, you will have to provide a function to decide equality of `var` (which seems to be `nat`, so there is probably such a function in the standard library too).
If you do not know the "{p} + {q}" notation, you can look it up here: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool
Problem
I'm trying to use the list remove function in Coq standard library but it asks for a bizarre typing and I don't know how to solve. The function I'm implementing is to make a list of free variables in a lambda term as follows: ``` Fixpoint fv (t : trm) : vars := match t with | Var v => [v] | App t1 t2 => (fv t1) ++ (fv t2) | Abs x t' => remove x (fv t') end. ``` And it gives me the following error: ``` Error: In environment fv : trm -> vars t : trm x : nat t' : trm The term "x" has type "nat" while it is expected to have type "forall x0 y : ?171, {x0 = y} + {x0 <> y}". ``` I'm pretty sure there is something to do with that hyphotesis thing in the definition of the remove function. I have no idea how to deal with it though, any helps?