對碼公式的左邊

Question

我需要使用nat_plus_commute.fold_set_fold_remdups碼公式，而不是Finite_Set.fold_def部分應用的不斷：

interpretation nat_plus_commute: comp_fun_commute "plus :: nat ⇒ nat ⇒ nat" 
    by standard auto 

declare Finite_Set.fold_def [code del] 
declare nat_plus_commute.fold_set_fold_remdups [code] 

的問題是，第一個方程只被定義爲plus操作，所以我得到以下警告：

Partially applied constant "Groups.plus_class.plus" on left hand side of equation, in theorem: 
Finite_Set.fold op + ?y (set ?xs) ≡ fold op + (remdups ?xs) ?y 

至於導致下面的語句

value "Finite_Set.fold plus 0 (set [1::nat, 2])" 

返回異常：

exception Fail raised (line 29 of "generated code"): Finite_Set.fold 

是否可以使用特定的操作（plus）和類型（nat）一個專門的代碼方程？

Answer 1

我不能肯定希望要實現，但要注意Finite_Set.fold是一種低層次的結構，它與實際可用的屬性等操作只能以相當大的努力，參見導出理論src/HOL/Finite_Set.thy和src/HOL/Groups_Big.thy有一個粗略的想法。

有關有限集合和列表求和，還有總和和sum_list其中已經裝備了代碼方程。