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.
```

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

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

@Pierre Roux Ah, indeed! Thanks a lot.

Last updated: Jul 13 2024 at 02:02 UTC