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确实隐含此论点吗？

杰森·格罗斯

没有。

cf错误＃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.

本文收集自互联网，转载请注明来源。

如有侵权，请联系 [email protected] 删除。