“结果包含获得的参数：b”是什么意思？在伊莎贝尔？
考虑以下代码片段：
lemma ejercicio_10_MSV2:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
{ assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" by (rule exE)}
命令 } 的调用给出以下错误：结果包含获得的参数：b。
Consider the following code fragment:
lemma ejercicio_10_MSV2:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
{ assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" by (rule exE)}
The invocation of the command } is giving the following error: Result contains obtained parameters: b.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您正在尝试将变量b从其自然范围中导出。您的方法看起来错误，我建议您尝试在“ p a”上进行案例分析。
You are trying to export the variable b out of its natural scope. Your approach looks wrong and I suggest that you try case analysis on “P a”.