fact: Definition representsDecl redundant ek mods modelField representsKind pred := let relational := match representsKind with | Functional => false | Relational => true end in TYPESPEC.REPRESENTS.Build_t (javaVisibility ek mods) modelField pred relational (typeSpec_isStatic ek mods) redundant.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)