はスコープ

Question

This answer内の表記を広げ、簡単な便利なトリックを提供します：unfold ">="はunfold geと同じですが、>=がgeの表記法であることを知っているあなたを必要としません。

スコープ内で表記法を同じにすることはできますか？それはge、ないN.geを展開しようとするため

ここ

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

unfold ">="は何もしません。

私は、次の解決策を発見した：

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を与えます。