鉴于此代码
locale A =
fixes foo :: "'a"
locale B = A +
fixes bar :: "'a × 'a"
locale C' = A +
fixes baz :: "'a"
begin
sublocale B foo "(foo, baz)".
end
I get
Type unification failed
Failed to meet type constraint:
Term: (foo, baz) :: 'b × 'a
Type: 'b × 'b
所以看来伊莎贝尔不明白baz and foo应该是同一类型。有没有办法来解决这个问题？
问题出在你的区域设置声明上B and C。声明为B等价于下面的
locale B = A foo for foo +
fixes bar :: "'a * 'a"
Locales 导入只记住参数的名称，而不记住类型变量的名称。因此，由于您没有指定类型foo，最通用的类型B的参数如下：
foo :: 'b
bar :: 'a * 'a
您可以使用命令看到这一点print_locale B。同样的情况也发生在 locale 的声明中C.
如果你想拥有相同的类型foo and bar，您必须在区域设置声明中明确连接。有两种方法可以做到这一点。
locale B = A foo
for foo :: 'a
+
fixes bar :: "'a * 'a"
and
locale B = A +
constrains foo :: 'a
fixes bar :: "'a * 'a"
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
