查找「卡」功能

Question

我很困惑確定設置基數的功能在哪裏精確定位。如果我在Cardinality.thy中查看 ，則不會找到任何內容，但會導入Phantom_Type，後者又導入Main，其中至少會找到縮寫card（雖然不是card本身的定義）。

Answer 1

就在伊莎貝爾/ jEdit的「卡」一詞在按住Ctrl鍵點擊，它會帶你直接到定義Finite_Set.thy：

text ‹ 
    The traditional definition 
    @{prop "card A ≡ LEAST n. ∃f. A = {f i |i. i < n}"} 
    is ugly to work with. 
    But now that we have @{const fold} things are easy: 
› 

global_interpretation card: folding "λ_. Suc" 0 
    defines card = "folding.F (λ_. Suc) 0" 
    by standard rule 

這裏使用了folding語言環境，它提供了一個操作摺疊（即迭代）在有限集合的元素上。

我不確定你在想什麼縮寫。如果您的意思是CARD('a)，那只是card (UNIV :: 'a set)的一些語法，即'a類型的基數。