Commit d0ecd1fe authored by Glen Mével's avatar Glen Mével
Browse files

minor: regroup notations for logical connectives

parent e3046298
......@@ -127,6 +127,12 @@ Notation "e1 ≠ e2" := (¬ (e1%E = e2%E))%E : expr_scope.
Notation "e1 ∧ e2" := (BinOp AndOp e1%E e2%E) : expr_scope.
Notation "e1 ∨ e2" := (BinOp OrOp e1%E e2%E) : expr_scope.
(* Short-circuited Boolean connectives *)
Notation "e1 && e2" :=
(If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
Notation "e1 || e2" :=
(If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
(* The breaking point '/ ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E)
......@@ -172,12 +178,6 @@ Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope.
(* Shortcircuit Boolean connectives *)
Notation "e1 && e2" :=
(If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
Notation "e1 || e2" :=
(If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
(** Notations for option *)
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment