问用Isabelle表示参数缩写
EN

Stack Overflow用户

提问于 2020-03-09 20:21:30

回答 1查看 41关注 0票数 1

我想删减一个点的等价类：

r `` {p}

至

[p]

在Isabelle中，什么才是正确的方法？

回答已采纳

发布于 2020-03-09 20:39:00

您只能在r固定的上下文中执行此操作，例如匿名上下文或区域设置：

context
  fixes r :: "('a × 'a) set"
begin

abbreviation foo ("⟨_⟩" 1000) where
  "⟨p⟩ ≡ r `` {p}"

我在这里使用了人字形而不是方括号，因为方括号会与列表的语法冲突，所以它

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/60600470

复制

相似问题

问用Isabelle表示参数缩写EN