Stream: Coq users

Topic: Associating Number notations with custom entries


view this post on Zulip Anton Trunov (Jul 02 2021 at 12:15):

How do I define a Number Notation for a Custom Entry so that I don't have to open any scopes or specify them by %scope?

For instance, I'd like to do something like this:

Inductive expr : Type :=
| Const : nat -> expr
| Plus : expr -> expr -> expr.

Declare Custom Entry expr.
Declare Scope expr_scope.
Delimit Scope expr_scope with expr.

Notation "<<< e >>>" := e (at level 0, e custom expr at level 99).

(* Number notation *)
Definition of_uint (u : Number.uint) : expr := Const (Nat.of_num_uint u).
Definition to_uint (e : expr) : option Number.uint := match e with Const n => Some (Nat.to_num_uint n) | _ => None end.

Number Notation expr of_uint to_uint : expr_scope.
Notation "x" := x (in custom expr at level 0, x constr at level 0) : expr_scope.
Notation "x + y" := (Plus x y) (in custom expr at level 50, left associativity) : expr_scope.

Check 42 : nat.
Fail Check <<< 42 >>> : expr.

view this post on Zulip Ali Caglayan (Jul 02 2021 at 14:36):

You need to open expr_scope, but I guess you are asking how to bind the scope to the notation?

view this post on Zulip Pierre Roux (Jul 02 2021 at 15:19):

Notation "<<< e >>>" := e%expr (at level 0, e custom expr at level 99).

view this post on Zulip Anton Trunov (Jul 02 2021 at 15:48):

@Pierre Roux Ah, indeed! Thanks a lot.


Last updated: Jan 29 2023 at 05:03 UTC