在语言环境中约束类型变量

Question

Isabelle 库包含类 real_inner 和 real_normed_vector，后者在 ~~src/HOL/Library/Inner_Product.thy.

中声明为前者的子类

现在，假设我们有一个语言环境

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

并希望用一些新常量扩展此语言环境，同时也将 'a 的排序限制为 real_inner，如下所示：

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

有办法吗？尝试使用上面的示例执行此操作时，Isabelle 在 extended 中给出了 '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"

Constraining type variables in locales