fact: Definition fieldModifierValue (ek:TypeDefKind) (fk:FieldKind) (mods:list Modifier) (m:Modifier) : bool := let m_present := existsb (eqb_Modifier m) mods in let instance_present := existsb (eqb_Modifier instance) mods in let ghost_present := existsb (eqb_Modifier ghost) mods in match m with | final => m_present || ((eqb_FieldKind fk FieldFK) && (eqb_TypeDefKind ek InterfaceEK) && (negb ghost_present)) | static => m_present || ((eqb_TypeDefKind ek InterfaceEK) && (negb instance_present)) | ghost => m_present | nullable => m_present | monitored => m_present | _ => 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)