如何在Isabelle/jEdit中启用"跟踪"

Question

我是vim粉丝,但只有emacs才有这个Isabelle/HOL环境.jEdit很棒,但我不能使用

using [[simp_trace=true]]

就像在emacs中一样.

如何在jEdit中启用"跟踪" ？

Answer 1

你确实可以simp_trace在Isabelle/jEdit的证据中使用,如下所示:

lemma "(2 :: nat) + 2 = 4"
  using [[simp_trace]]
  apply simp
  done

或者,您可以全局声明它,如下所示:

declare [[simp_trace]]

lemma "(2 :: nat) + 2 = 4"
  apply simp
  done

当光标apply simp位于jEdit中的语句之后时,两者都会在"输出"窗口中为您提供简化器的跟踪.

Answer 2

如果您需要的深度超过1(默认值),则需要对其进行微调

declare [[simp_trace_depth_limit=4]] 

然后,此示例的跟踪深度为4.