如何隐式设置节中所有出现的变量

Question

让我们以这样的例子为例Section

Section myList.

Variable X : Type.

Definition myListApp2 (l1 l2       : list X) :=
  app l1 l2.

Definition myListApp3 (l1 l2 l3    : list X) :=
  app (app l1 l2) l3.

Definition NoXUse n := S n.

Definition myListApp4 (l1 l2 l3 l4 : list X) :=
  app (app (app l1 l2) l3) l4.

End myList.

Arguments myListApp2 {X}.
Arguments myListApp3 {X}.
Arguments myListApp4 {X}.

在End的Section之后，我需要手工设置所有隐式定义的第一个参数，有没有办法告诉Coq Variable X总是隐式的？

Answer 1

Context command是Context的变体，允许这样做。

Variable