fact: Definition varDecl (mods:list Modifier) (t:StaticType) (name:VarName) : Var := VAR.Build_t (VARSIGNATURE.Build_t name t) (hasModifier mods final) (negb (hasModifier mods non_null)) (hasModifier mods ghost) (hasModifier mods uninitialized).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)