fact: Definition eq_primitiveType (x y:primitiveType) : bool := match x, y with | BOOLEAN, BOOLEAN => true | BYTE, BYTE => true | SHORT, SHORT => true | INT, INT => true | _, _ => false end.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)