查找“卡”功能

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类型的基数。