在范围内展开记号

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。