Coq 计算类型中的隐式参数
Implicit arguments in a computed type in 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 确实隐含这个论点?
没有
C.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.
我有一个库可以编写索引类型,而无需显式线程化索引。通过隐藏不相关的管道,这会导致更清晰的顶级类型。它是这样的:
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 确实隐含这个论点?
没有
C.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.