时间戳

首页 > 解决方案 > 如何在部分隐式中设置所有出现的变量

coq - 如何在部分隐式中设置所有出现的变量

问题描述

让我们以这样的事情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有没有办法告诉 CoqVariable X总是隐式的？

标签： coq

解决方案

该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.

推荐阅读