Изабель и класс перегрузки

Question

двух классов определены, содержащие ту же самую функцию, но когда эти два класса используют в местности есть ошибка объединения:

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 б) (getName_b b) и использовать определение класса

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

Существует ли решение без переименования?

Here решение предоставляется, когда перегрузка необходима, когда типы данных являются параметрами.

Answer 1

Можно использовать полные или частично квалифицированные идентификаторы. Я использовал find_consts, как показано ниже, чтобы найти квалифицированные имена констант класса типов.

Тип вывода требует только, чтобы я использовал 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