set - Coq 中使用 fun 的 Curry-Howard 同构定义

Question

我在 Coq 中定义时遇到了一些问题，尤其是在使用 CHI 定义时。我已经设法获得了对基本原则的理解，但是当我尝试定义这一点时”

((A -> (A -> C)) * ((A -> C) -> A)) -> C :=

我一无所获，因为它一直告诉我：
"Error: The type of this term is a product while it is expected to be "C"。
我已经尝试过我之前在脚本中使用过的常用策略，并且我确信必须使用相同的方法（有趣）来解决这个问题，但是我似乎正在尝试的一切都以该错误消息结尾。有小费吗？

Answer 1

您似乎正在定义一个作为输入的函数：

• 一个类型的函数A -> (A -> C)：给定一个类型的对象A，它返回一个类型的函数A -> C。
• 一个类型的函数(A -> C) -> A：给定一个类型的函数A -> C，它返回一个类型的对象A。

您正在尝试构建一个类型的对象C，我不知道您将如何设法做到这一点。A但是，您可以通过组合作为输入的两个函数来构建类型对象。

希望能帮助到你，

五。