목록 제거 기능 사용

Question

Coq standard library의 목록 제거 기능을 사용하려고하지만 기괴한 입력을 요구하며 해결 방법을 모르겠습니다.

는

내가 구현하고있어 기능은 다음과 같이 람다 관점에서 자유 변수의 목록을 만드는 것입니다 :

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. 

을 그리고 그것은 나에게 다음과 같은 오류 제공 : 난

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}". 

을 remove 함수의 정의에서 그 위선 사물과 관련이 있는지 확실히 알 수 있습니다. 그래도 어떻게 대처해야할지 모르겠다. 함수는 제거

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

은 (Print remove.을 수행하여 볼 수있는) 제 인수로이 소요

이 가설의 요소 어떤지를 결정하는 함수는 :

Answer 1

remove을 포함하는 컨텍스트에 정의 된 너의 명부에있는 유형의. 귀하의 경우에는 (이는 nat 인 것 같음)을 결정하는 함수를 제공해야하므로 표준 라이브러리에도 그러한 함수가있을 수 있습니다. 당신이 "{P} + {Q}을"알 수없는 경우

표기, 당신은 여기를 찾아 볼 수 있습니다 : http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool