coq - Coq 中的对和预测

Question

我从https://coq.inria.fr/library/Coq.Init.Datatypes.html获取以下代码：

Inductive prod (A B:Type) : Type :=
  pair : A -> B -> A * B

where "x * y" := (prod x y) : type_scope.

Add Printing Let prod.

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.



Section projections.
  Context {A : Type} {B : Type}.

  Definition fst (p:A * B) := match p with (x, y) => x end.
  Definition snd (p:A * B) := match p with (x, y) => y end.


End projections.

当我将它加载到 CoqIDE 中时，Definition fst...它会出现消息The constructor pair (in type prod) expects 4 arguments.。我该如何解决这个问题？

标签： coq

Answer 1

添加

Set Implicit Arguments.

到文件的顶部。