Механизм сечения в Coq.Запретить опускание гипотез из контекста

Question

Мне нужен более примитивный механизм обобщения в разделах.Например,

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

Я получу Q: Set, но мне нужно Q: nat-> Set.

Я пробовал Контекст, Гипотезы, Переменные.Не работаетКак получить такое поведение?

Answer 1

Это не то, что вы можете сделать с Definition ... := Однако вы можете использовать Proof using:

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