CODEWITHSUNDEEP
coq
Zimm i48
Zimm i48

Reputation: 3061

Unfold a notation within a scope

This answer provides a simple useful trick: unfold ">=" is the same as unfold ge but does not require you to know that >= is the notation for ge.

Can you do the same for notations within a scope?

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

Here unfold ">=" does not do anything because it tries to unfold ge, not N.ge.

I have found the following solution:

Open Scope N.
unfold ">=".

But is there a syntax allowing to unfold this notation without first opening the scope?

Upvotes: 1

Views: 636

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15404

Yes, you can use the template unfold string % scope as follows:

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

This gives us the goal forall x : N, (x ?= x)%N <> Lt with unfolded >=.

Upvotes: 1

Related Questions