伊莎贝尔和 class 重载

Question

定义了两个 classes 包含相同的功能，但是当这两个 classes 在语言环境中使用时会出现统一错误：

theory Scratch
imports Main 
begin


  class c1 =
    fixes getName :: "'a ⇒ string"

  class c2 =
    fixes getName :: "'a ⇒ string"

  locale c12 = 
    fixes match :: "('a::c1) ⇒ ('b::c2) ⇒ bool"
    assumes as : "match a b ⟶ (getName a) = (getName b)"

end

通过将 (getName b) 重命名为 (getName_b b) 并使用 class 定义

来解决统一错误

  class c2 =
    fixes getName_b :: "'a ⇒ string"

有不重命名的解决方案吗？

Here当数据类型为参数时需要重载时给出解决方案。

Answer 1

可以使用完全或部分限定的标识符。如下所示，我使用 find_consts 来查找类型 class 常量的限定名称。

类型推断只需要我使用 c1_class.getName a 来消除错误。

theory Scratch
imports Complex_Main
begin
class c1 =
  fixes getName :: "'a => string"

class c2 =
  fixes getName :: "'a => string"

find_consts name: getName (*
  find_consts
  name: "getName"

  found 2 constant(s):
    Scratch.c1_class.getName :: "'a => char list"
    Scratch.c2_class.getName :: "'a => char list"
*)

declare[[show_sorts]]
locale c12 = 
  fixes match :: "('a::c1) => ('b::c2) => bool"
  assumes as : "match a b --> (c1_class.getName a) = (getName b)"

end

伊莎贝尔和 class 重载

Isabelle and class overloading

isabelle