0

我刚刚写了这段代码：

lemmas gc_step_intros =
  normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
  normal[OF step.intros(4)] normal[OF step.intros(5)] drop

其中step.intros实际上只有 5 个引理。有没有一种方便的方法来避免这种重复，即看起来像下面这样的东西？

lemmas gc_step_intros = normal[OF_EACH step.intros] drop
4

1 回答 1

1

您可以使用THEN而不是OF利用属性应用于定理列表中的所有定理这一事实。以下应该做你想要的：

lemmas gc_step_intros = step.intros[THEN normal] drop
于 2014-10-29T14:09:42.180 回答