约束区域设置中的类型变量

Question

Isabelle 库包含类 real_inner 和 real_normed_vector，后者在 ~~src/HOL/Library/Inner_Product.thy 中声明为前者的子类。

现在，假设我们有一个区域设置

locale foo =
  fixes goo :: "'a::{real_normed_vector} => bool"

并希望使用一些新常量扩展此语言环境，并同时限制要real_inner的'a类型，如下所示：

locale extended = foo +
  fixes ext :: "'a::{real_inner} => nat"

有没有办法做到这一点？ 尝试使用上面的例子来做到这一点，看到 Isabelle 在 extended 中给 goo 'b::{real_normed_vector} => bool类型，而我反而需要类型 'a::{real_inner} => bool .

Answer 1

你可以

这样做：

locale extended = foo goo
  for goo :: "'a :: real_inner ⇒ bool" +
  fixes ext :: "'a => nat"