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
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: Jan 29 2023 at 05:03 UTC