我想简化一点的等价类：
r `` {p}
至
[p]
在伊莎贝尔，正确的做法是什么？
您只能在r固定的上下文中执行此操作，例如匿名上下文或语言环境：
context
fixes r :: "('a × 'a) set"
begin
abbreviation foo ("⟨_⟩" 1000) where
"⟨p⟩ ≡ r `` {p}"
我在这里使用人字形代替括号，因为括号会与列表的语法冲突，所以它会
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句