Coq : 인수의 인수에 패턴 매칭을 통한 함수 정의

Question

함수를 정의하려면 함수의 인수가 (적어도) n 위치 함수인지 여부에 따라 달라집니다. 초보 (실패) 시도 rT는 False에 모든 매핑,

Definition rT {y:Type}(x:y) := ltac: (match y with 
| _ -> _ -> _ => exact True 
| _ => exact False end). 

Check prod: Type -> Type -> Type. 
Compute rT prod. (*= False: Prop*) 
Print rT. (*rT = fun (y : Type) (_ : y) => False: forall y : Type, y -> Prop*) 

보시다시피

입니다. 왜? 일치 조항에서 y을 바꾸면 결과가 동일하게 유지됩니다. type of x

Answer 1

원하는 기능이 원하는 유형의 Gallina 내에 존재할 수 없습니다.

귀하의 기능이 허용됩니다,하지만 당신은 그것을 인쇄하는 경우, 당신은 몸이 볼 수

rT = fun (y : Type) (_ : y) => False 

갈리나는 Type에 -ing match 방법이 없습니다. n-ary 함수를 처리 할 수있는 방법이 있습니다. 이러한 방식으로 해당 요소를 검사 할 수 있지만 종속성 유형을 사용하면 정적을 정적으로 캡처 할 수 있습니다. 예를 들어, 균일 한 n 차 기능 :

https://coq.inria.fr/library/Coq.Numbers.NaryFunctions.html