Coq

2017-11-09 102 views
7

'da hesaplanan türdeki örtülü bağımsız değişkenler Dizini açıkça işlemek zorunda kalmadan dizinlenmiş türleri yazmak için bir kitaplığım var. Bu, ilgisiz sıhhi tesisatın yerini gizleyerek üst düzey tiplerin daha temiz olmasını sağlar. gösterildiği gibiCoq

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). 

Ancak Coq örtülü IForall getirdiği evrensel niceleyici yapmak benim isteği yok sayar:

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

beni almak için bir yolu var mı Böyle bir şey gider Coq gerçekten bu argümanı örtülü kılıyor mu?

+0

böyle bir gösterim tanımlarsanız bunu denedim ama henüz: 'Notasyonların ": fun var => body ": = (eğlenceli n var => gövde) (level ) .', daha sonra" Tanımlama kimliği {A: nat -> Type}: [A: -> A]: =: fun a = > a çalışmalıdır. Aradığın şeyin bu olduğundan emin değilim. –

+0

Ancak bazen herhangi bir şeyi bağlamak istemiyorum. Örneğin. Tanımlama uygulamasını (f: [A: -> B]) (a: [A]): ​​[B]): = f a. – gallais

cevap

2

No.

C.f. Bug #3357

Bir gün, PR #668 birleştirilecek ve sonra yapmanız mümkün olacak, umut

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.