fact: Definition specVisibility (ek:TypeDefKind) (mods:list Modifier) : Visibility := let fix specVisibility' (mods':list Modifier) : option Visibility := match mods' with | spec_public::_ => Some Spec_Public | spec_protected::_ => Some Spec_Protected | _::xs => specVisibility' xs | nil => None end in match (specVisibility' mods) with | Some v => v | None => javaVisibility ek mods end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)