Coq에서 계산 된 형식의 암시 적 인수

명시 적으로 인덱스를 스레드 할 필요없이 인덱싱 된 형식을 쓰는 라이브러리가 있습니다. 이것은 관련없는 배관을 숨겨서 더 깨끗한 최상위 유형으로 이어집니다. 에 의해 입증 된 바와 같이Coq에서 계산 된 형식의 암시 적 인수

Section Indexed. 

Local Open Scope type. 
Context {I : Type} (T : Type) (A B : I -> Type). 

Definition IArrow : I -> Type := 
    fun i => A i -> B i. 

Definition IForall : Type := 
    forall {i}, A i. 

End Indexed. 

Notation "A :-> B" := (IArrow A B) (at level 20, right associativity). 
Notation "[ A ]" := (IForall A) (at level 70).

그러나 COQ 암시 IForall에 의해 도입 된 보편적 정량을 내 요청을 무시 :

Fail Definition id {A : nat -> Type} : [ A :-> A ] := fun a => a. 
Definition id {A : nat -> Type} : [ A :-> A ] := fun (n : nat) a => a.

내가 얻을 수있는 방법이 있나요 그것은 이런 식입니다 Coq가 실제로이 주장을 함축적으로 만들까요?

출처

2017-11-09 gallais

우리는이 같은 표기법을 정의하면 내가 그것을 시도했지만되지 않은 :'표기법을 " 재미있는 var => body ": = (fun n var => body) (레벨 )''이면,'정의 id {A : nat -> 타입} : [A : -> A] : = : fun a = > a.' 작동해야합니다. 이것이 당신이 찾고있는 것인지 확실하지 않습니다. –

하지만 가끔은 아무 것도 묶고 싶지 않습니다. 예 : 나는'정의 앱 (f : [A : -> B]) (a : [A]) : [b]) : = f a.'을 상자에서 꺼내고 싶습니다. – gallais

f. Bug #3357

어느 날, 나는 PR #668 병합 할 것, 그리고 당신이 할 수있을 것입니다 희망

Notation IArrow A B := 
    (fun i => A i -> B i) 

Notation IForall A := 
    (forall {i}, A i). 

Notation "A :-> B" := (IArrow A B) (at level 20, right associativity). 
Notation "[ A ]" := (IForall A) (at level 70). 

Definition id {A : nat -> Type} : [ A :-> A ] := fun a => a. 
Definition id {A : nat -> Type} : [ A :-> A ] := fun (n : nat) a => a.

출처

2017-11-19 07:54:50

Coq에서 계산 된 형식의 암시 적 인수

답변

관련 문제