fact: Definition EvalBinaryIntOp (op : BinaryIntOp) (i1 : Int.t) (i2 : Int.t) : Int.t := match op with | Addition => Int.add i1 i2 | Subtraction => Int.sub i1 i2 | Multiplication => Int.mul i1 i2 | Division => Int.div i1 i2 | Remainder => Int.rem i1 i2 | ShiftRightSigned => Int.shr i1 i2 | ShiftRightUnsigned => Int.ushr i1 i2 | ShiftLeft => Int.shl i1 i2 | BitwiseAnd => Int.and i1 i2 | BitwiseOr => Int.or i1 i2 | BitwiseXor => Int.xor i1 i2 end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)