Geek Answers Handbook

Using the delete list function

I try to use the delete list function in the Coq standard library , but it asks for a strange typing, and I don't know how to solve it.

The function I am implementing is to create a list of free variables in lambda terms 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 this 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 am sure there is something related to this hypothesis function in the definition of the remove function. I have no idea how to deal with this, but it helps?

+4
source share
1 answer

remove defined in a context containing:

Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.

The removees function takes this as the first argument (which you can see by doing Print remove.)

- , . var ( nat, ).

"{p} + {q}", : http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool

+4

More articles:


All Articles