如何编写这个coq代码的agda等效代码？

【问题标题】：How to write agda equivalent code of this coq code?如何编写这个coq代码的agda等效代码？
【发布时间】：2015-07-28 21:07:28
【问题描述】：

我想在 agda 中编写给定的 coq 代码。

Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x.

这种方式我试过了..

data included (D1 D2 : R -> Set) : Set where
      forall x : R D1 x -> D2 x

我知道问题出在第二行，但如何解决。我们需要定义构造函数吗？我将如何做到这一点？

请帮忙。

【问题讨论】：

标签： coq agda

【解决方案1】：

Agda 中的data 相当于 Coq 中的Inductive：它引入了一种以归纳方式定义的新类型。

在 Agda 中，Definition 的等价物只是您想要定义的事物的定义方程式：

postulate R : Set

included : (_ _ : R → Set) → Set
included D1 D2 = ∀ x → D1 x → D2 x

【讨论】：