时间戳

首页 > 解决方案 > 单例类中的隐式参数

coq - 单例类中的隐式参数

问题描述

当我以通常的语法使用单个方法创建类型类时，我可以给它隐式参数：

Class Foo1 := { foo1 {n} : Int n }.

但是当我使用单例语法时，我不能给它隐式参数

Fail Class Foo2 := foo2 {n} : Int n.

错误：语法错误：'.' 预计在 [gallina] 之后（在 [vernac_aux] 中）。

我什至不能Arguments用来使该参数隐含：

Class Foo3 := foo3 n : Int n.
Fail Arguments foo3 {n}.

该命令确实失败并显示消息：Flag "rename" expected to rename Foo3 into n。

它有理由这样工作吗？

标签： coq

解决方案

在你的第二次尝试

您的第二次尝试可以通过移动n冒号的另一侧来工作：

Class Foo2 := foo2 : forall {n}, Int n.

第三次尝试

错误消息告诉您使用该rename标志。这是因为foo3实际上将Foo3（它投射的类型类实例）作为第一个（隐式）参数，在整数之前。第一个参数恰好已经有一个名称 ( Foo3)，您可以通过运行看到About foo3.

About foo3.
(*
foo3 : Foo3 -> forall n : nat, Int n

Arguments foo3 {Foo3} _%nat_scope
*)

因此 Coq 认为您想将该参数重命名为n. 如果这确实是您想要的，您可以rename按照建议使用标志：

Arguments foo3 {n} : rename.

之后About foo3.将产生：

foo3 : Foo3 -> forall n0 : nat, Int n0

Arguments foo3 {n} n%nat_scope
  (where some original arguments have been renamed)

但是您真正想要的是通过使其隐含来影响第二个参数。在此过程中，您不想给它一个新名称（不需要，它已经命名n），并且您不想更改第一个参数（即保持隐含并避免重命名它）。因此，您应该做的是：

Arguments foo3 {_ _}.

屈服

Arguments foo3 {Foo3} {n}%nat_scope

推荐阅读