Anton Trunov (Jul 02 2021 at 12:15): 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.
You need to open expr_scope, but I guess you are asking how to bind the scope to the notation?
Pierre Roux (Jul 02 2021 at 15:19):Notation "<<< e >>>" := e%expr (at level 0, e custom expr at level 99).
@Pierre Roux Ah, indeed! Thanks a lot.
Last updated: Apr 19 2024 at 11:02 UTC