Skip to content
Snippets Groups Projects
Commit 5f858a94 authored by Ralf Jung's avatar Ralf Jung
Browse files

explain our choice of integer division operator

parent 32b4b0cc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
iris_heap_lang/lang.v
+ 3
− 0
View file @ 5f858a94
...@@ -79,6 +79,9 @@ Inductive base_lit : Set := ...@@ -79,6 +79,9 @@ Inductive base_lit : Set :=
Inductive un_op : Set := Inductive un_op : Set :=
| NegOp | MinusUnOp. | NegOp | MinusUnOp.
Inductive bin_op : Set := Inductive bin_op : Set :=
(** We use "quot" and "rem" instead of "div" and "mod" to
better match the behavior of 'real' languages:
-30/-4 == 7. ("div" would return 8.) *)
| PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *) | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
| AndOp | OrOp | XorOp (* Bitwise *) | AndOp | OrOp | XorOp (* Bitwise *)
| ShiftLOp | ShiftROp (* Shifts *) | ShiftLOp | ShiftROp (* Shifts *)
......
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