fact: Definition eqb_Modifier (x y:Modifier) := match x, y with | public, public => true | protected, protected => true | private, private => true | abstract, abstract => true | static, static => true | final, final => true | native, native => true | spec_public, spec_public => true | spec_protected, spec_protected => true | model, model => true | ghost, ghost => true | pure, pure => true | instance, instance => true | helper, helper => true | non_null, non_null => true | nullable, nullable => true | nullable_by_default, nullable_by_default => true | monitored, monitored => true | uninitialized, uninitialized => true | code, code => true | implicit_constructor, implicit_constructor => true | _, _ => false end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)