在范围内展开表示法

Question

This answer提供了一个简单的有用技巧：unfold ">="与unfold ge相同，但不要求您知道>=是ge的表示法。

对于范围内的符号，您也能这样做吗？

Require Import NArith.
Goal forall x, (x >= x)%N.
unfold ">=".

在这里，unfold ">="什么也不做，因为它试图展开ge，而不是N.ge。

我找到了以下解决办法：

Open Scope N.
unfold ">=".

但是，是否有允许在不首先打开作用域的情况下展开此表示法的语法？

Answer 1

是的，您可以按以下方式使用模板unfold string % scope：

Require Import NArith.
Goal forall x, (x >= x)%N.
  unfold ">=" % N.

这给了我们展开forall x : N, (x ?= x)%N <> Lt的目标>=。