coq - Coq 中的部分机制。禁止从上下文中省略假设

Question

我需要更原始的分段泛化机制。例如，

Section sec.
Context (n:nat).
Definition Q:=bool.
End sec.
Check Q.

我将获得 Q:Set，但我需要 Q:nat->Set。

我试过上下文、假设、变量。它不起作用。如何获得这样的行为？

标签： coq

Answer 1

这不是您可以做的事情Definition ... := 但是，您可以使用Proof using：

Section sec.
Context (n:nat).
Definition Q : Set.
Proof using n.
  exact bool.
Defined.
End sec.
Check Q.