Как установить все вхождения переменной в разделе неявным - PullRequest
Новая
       46

Как установить все вхождения переменной в разделе неявным

1 голос
/ 14 апреля 2020

Давайте подумаем о чем-то подобном 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 всегда неявно?

1 Ответ

2 голосов
/ 14 апреля 2020

Команда Context является вариантом Variable, который позволяет это. 

Section myList.

Context {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.
...