Commit dfdac9cb authored by Léon Gondelman's avatar Léon Gondelman

wip on notations

parent 6fbbda09
...@@ -15,8 +15,22 @@ Notation "e1 ;ᶜ e2" := (e1%E ;;;; e2%E) ...@@ -15,8 +15,22 @@ Notation "e1 ;ᶜ e2" := (e1%E ;;;; e2%E)
(at level 100, e2 at level 200, (at level 100, e2 at level 200,
format "'[' '[hv' '[' e1 ']' ;ᶜ ']' '/' e2 ']'") : expr_scope. format "'[' '[hv' '[' e1 ']' ;ᶜ ']' '/' e2 ']'") : expr_scope.
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope. Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope. Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
(a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
(at level 200, e1, e2, e3 at level 200, only parsing) : expr_scope.
Notation "'whileᶜ' ( e1 ) { e2 } " := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
(at level 200, e1, e2 at level 200, only parsing) : expr_scope.
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