fix <> notation for BAnon

heap_lang/lang.v

@@ -16,12 +16,12 @@ Inductive bin_op : Set :=
   | PlusOp | MinusOp | LeOp | LtOp | EqOp.
 
 Inductive binder := BAnon | BNamed : string → binder.
+Delimit Scope binder_scope with bind.
+Bind Scope binder_scope with binder.
 
 Definition cons_binder (mx : binder) (X : list string) : list string :=
   match mx with BAnon => X | BNamed x => x :: X end.
 Infix ":b:" := cons_binder (at level 60, right associativity).
-Delimit Scope binder_scope with bind.
-Bind Scope binder_scope with binder.
 Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
 Proof. solve_decision. Defined.
 

heap_lang/notation.v

@@ -16,7 +16,6 @@ Coercion of_val : val >-> expr.
 
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
-Notation "<>" := BAnon : expr_scope.
 
 (* No scope for the values, does not conflict and scope is often not inferred properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
@@ -35,10 +34,10 @@ Notation "^^ e" := (wexpr' e%E) (at level 8, format "^^ e") : expr_scope.
 Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
 Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
-  (Match e0 x1 e1 x2 e2)
+  (Match e0 x1%bind e1 x2%bind e2)
   (e0, x1, e1, x2, e2 at level 200) : expr_scope.
 Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
-  (Match e0 x2 e2 x1 e1)
+  (Match e0 x2%bind e2 x1%bind e1)
   (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
 Notation "()" := LitUnit : val_scope.
 Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
@@ -56,9 +55,9 @@ Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
 Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
-Notation "'rec:' f x := e" := (Rec f x e%E)
+Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
   (at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x := e" := (RecV f x e%E)
+Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
   (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (at level 200, e1, e2, e3 at level 200) : expr_scope.
@@ -67,30 +66,30 @@ Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
 are stated explicitly instead of relying on the Notations Let and Seq as
 defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
-Notation "'rec:' f x y := e" := (Rec f x (Lam y e%E))
+Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%E))
   (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y := e" := (RecV f x (Lam y e%E))
+Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
   (at level 102, f, x, y at level 1, e at level 200) : val_scope.
-Notation "'rec:' f x y .. z := e" := (Rec f x (Lam y .. (Lam z e%E) ..))
+Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y .. z := e" := (RecV f x (Lam y .. (Lam z e%E) ..))
+Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
 
-Notation "λ: x , e" := (Lam x  e%E)
+Notation "λ: x , e" := (Lam x%bind e%E)
   (at level 102, x at level 1, e at level 200) : expr_scope.
-Notation "λ: x y .. z , e" := (Lam x (Lam y .. (Lam z e%E) ..))
+Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
   (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "λ: x , e" := (LamV x e%E)
+Notation "λ: x , e" := (LamV x%bind e%E)
   (at level 102, x at level 1, e at level 200) : val_scope.
-Notation "λ: x y .. z , e" := (LamV x (Lam y .. (Lam z e%E) .. ))
+Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
   (at level 102, x, y, z at level 1, e at level 200) : val_scope.
 
-Notation "'let:' x := e1 'in' e2" := (Lam x e2%E e1%E)
+Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
 Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
 (* These are not actually values, but we want them to be pretty-printed. *)
-Notation "'let:' x := e1 'in' e2" := (LamV x e2%E e1%E)
+Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
 Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.