Открываются нотацию в пределах области

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 с развернутым >=.