diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v index f435cb81c792230cadb7fe30e5e8013bb590bcdc..6a126402e27acbf9923eb42d97156476c3067bac 100644 --- a/iris_heap_lang/lang.v +++ b/iris_heap_lang/lang.v @@ -79,6 +79,9 @@ Inductive base_lit : Set := Inductive un_op : Set := | NegOp | MinusUnOp. 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 *) | AndOp | OrOp | XorOp (* Bitwise *) | ShiftLOp | ShiftROp (* Shifts *)